The Test Was a Submission.

One small claim, no special lane

The candidate adds a degree consequence to an existing polynomial result: over a characteristic-zero integral domain, a polynomial unchanged by translation through a nonzero element has natural degree zero. It changes one subject module and adds one immutable claim record. No workflow, policy, documentation, test, or generated-receiver file travelled with it.

That is intentionally ordinary. It is not offered as new mathematics or as a benchmark of theorem discovery. It is a real importable corollary, built in the public library shape, and the sort of compact extension a contributor could send.

Two independent runs

First the local receiver ran against origin/main after a full lake build. It accepted the candidate in 75 seconds. The report records the changed paths, the axiom closure, no exact Mathlib match, a downstream import pass, and a kernel replay pass.

Then the pull request ran the trusted GitHub receiver. Its workflow checked out the trusted base-side validator separately from the untrusted candidate, repeated cheap preflight, acquired the pinned dependency cache, and ran restricted formal validation. The Python suite and release-upgrade gate were green; the authoritative validate job was green too.

The claim and its receiver observation are now durable corpus material. The generated catalogue gained the entry without an editorial rewrite.

The merge is evidence too

The author was on the repository's narrow auto-merge allowlist. Once the trusted receiver accepted the current pull-request base, the ordinary PR merged automatically. No person evaluated whether the theorem was important, elegant, or explainable. The allowlist was a permission to apply a machine verdict, not a second admission criterion.

This is the small distinction the public instructions now make explicit: an accepted report decides admission for everyone; automatic merge is only available to accounts the repository permits to use that mechanism. Other accepted work waits for a maintainer to apply the same result.

What one green run does and does not say

This is one post-upgrade end-to-end success, not a proof that the receiver has no defects. It does establish something narrower and valuable: the release policy, fresh dependency pair, local command, trusted candidate separation, restricted audit, observation generator, catalogue generator, and auto-merge route were all exercised together on an ordinary contribution.

That is the only kind of confidence this project is trying to accumulate: specific claims, attached to specific runs, with the next submission free to contradict them.