Nobody Clicked Merge.

The gate was a person

Every submission had waited for someone to click merge. The branch ruleset already required zero approving reviews and the repository already permitted auto-merge, so nothing was missing but the call — and a decision about whose submissions the machine may land on its own.

That decision is an allowlist, read from the default branch and never from the candidate, because a submission able to extend it would be approving itself. Branches under maintenance/ are excluded: they carry receiver, policy and workflow changes, and infrastructure should not land unattended even when mathematics does. Since then four submissions have merged with leanfrontier-receiver[bot] as the merging identity, and two of those went from opened to merged in four minutes.

The mechanism runs on workflow_run rather than on the pull request, because a fork's pull-request token is read-only and carries no secrets — the same wall that broke the observation writer in an earlier note. It also refuses to merge a pull request that has moved past the commit which was validated.

A hypothesis the launcher was suppressing

The task launcher told producers to prefer an uncovered area. That points away from the corpus, so the sparse dependency graph this project has been measuring may have been an artefact of its own instruction rather than a property of machine mathematics.

There are now two launchers, differing in exactly one paragraph, and a test asserts the two files stay word-identical everywhere else so nothing drifts in as a second unrecorded treatment. The hypothesis, the metric, the stopping point of eighteen accepted submissions per arm, the power table behind that number, and a commitment to report a null as no effect larger than about four times rather than no accumulation were all fixed in advance, while the assignment ledger was still empty.

Three submissions carry an arm so far. The two under the original wording opened fresh subjects and imported nothing. The one under the extension wording imported LeanFrontier.NumberTheory.SternDiatomic and proved the enumeration theorem on top of it — the substantive result of that area rather than a restatement. That is one submission per arm and it establishes nothing; the stopping rule is eighteen for exactly this reason. It is the shape the hypothesis predicts, on the first attempt.

Stating without proving

A conjecture needs no sorry. A definition whose type is literally Prop asserts nothing — the kernel confirms the right-hand side is a well-formed proposition and no more — so it passes elaboration, the axiom closure, the sorry scan and the kernel replay unchanged. The trust boundary does not move at all.

The fingerprint has to come from the value rather than the type, since every conjecture's type is the same Prop. Done that way, a conjecture restating Nat.add_comm produces a digest already present among the 466,700 entries in the pinned index, so restating known mathematics is rejected as a duplicate with no new code. Conjectures are probed in both directions, and stating is bound to proving: a producer may hold one unresolved conjecture per accepted theorem they have landed, so a producer who has landed none may state none.

Nobody has stated one yet. The corpus contains zero.

What running it found that thinking about it had not

Six defects surfaced in a day, and the ratio is the point: one came from review, five came from something actually going through the pipeline.

The schema gained a field while the validator kept its own hardcoded key set, so the receiver rejected a claim the schema permits — and only in continuous integration, because the client stamped the field after validating and pushed something it had never checked. A test asserted the assignment ledger was current, which is false by construction on any pull request that adds a submission, since the ledger is written after the merge; it would have failed every submission in perpetuity. The trusted writer began committing a path the trusted gate's allowlist did not mention, so the writer opened pull requests the gate refused. The conjecture quota and both probes read the claim's entrypoints, so a producer who simply omitted a conjecture from the claim faced no quota and no probing. A producer's branch went stale because an agent run takes long enough that generated pull requests merge underneath it. And an agent in a headless session hit a permission prompt for reading git history and asked for approval nobody was there to give.

Three of those are the same shape: one key set held in two places. Each now has a test deriving one from the other, which is the only way that stays true.

The number that has not moved

Twenty-nine accepted submissions, twenty-nine modules, five internal import edges. That is 0.17 per module, where it was 0.17 per module yesterday. Only the extension-arm submission added one.

Two further submissions arrived today from a different producer and are recorded as unassigned, deliberately: they are outside the experiment, and putting a non-client submission into an arm would contaminate it. One proves that a polynomial over a characteristic-zero integral domain invariant under a nonzero translation must be constant. The other gives the sum of all pairwise squared differences over a finite set in terms of the sum of squares and the square of the sum — the variance identity in unnormalised form, over an arbitrary commutative ring. Neither imports anything from the corpus.

What this was

Twelve merged changes, four submissions nobody approved, and a pre-registration that is now binding rather than aspirational.

The honest summary is the same one the previous note ended on, confirmed rather than repeated. Reasoning found the launcher wording. Running found the schema split, the impossible test, the gate mismatch, the ordering bug, the opt-in quota and the stale branch. That is an argument for producing rather than for hardening, which remains inconvenient, because hardening is the part that feels responsible.