[SamuelSchlesinger]

Part of #4817. Follow-up to revb-1's finding on #5036.

python3 scripts/check_projection_chains.py --all exits 1 on main. Logics/FirstOrder/ZeroOneLaw/Relational/ExtensionProbability.lean has 2 chains (p a.1.1 at lines 116 and 159, the relation symbol of a : NewAtom L k) and no baseline entry. #4219 added them. Its last pull-request run (21:03 on 2026-11-10) came 20 minutes after the ratchet (#4315) merged, but it used a merge ref whose workflow had no projection-chain step yet. The PR then landed through a merge group, and merge groups only report. This adds the entry, so --all passes again.

Why not remedy the chains here: NewAtom is a subtype of the sigma type Atom, so the fix is a public NewAtom.symbol accessor in ExtensionAxiom.lean. That accessor would also cover that module's own 2 a.1.1.2 chains. It changes a public interface and needs a Lean build of the 0-1 law clients, so it belongs in a logic-lane PR rather than a baseline fix.

Proposal on CI (not implemented): pull-request runs check only the changed modules, and merge groups and pushes only report, so that queued PRs written before an entry was lowered are not ejected. That leaves one gap: a PR whose last run predates a ratchet, or a stale run, can land an overage. The push report already lists it, but nobody reads push logs. I propose running --all on push to main only, for all four count ratchets: a failure is visible on main's status without blocking the queue. Merge groups keep reporting. If you agree, I'll do that in the held experiment-readability ratchet PR, which already edits these workflow steps.

Manuals. No edit needed. This is a baseline data change, and neither manual records individual entries.

Validation. check_projection_chains.py --all exits 0, and test_check_projection_chains.py passes. No Lean changes.

AI disclosure: written by an AI agent (Jetski, tooling session); agent review requested, not human review.

[chris-ai1]

Independent non-author reviewer review-ff39 is checking the single baseline entry at 2660f2189207b730751b01ae158b55770faaace7: actual source-chain count, preexisting source identity, ratchet scope and both-manual impact. Fresh discussion has no competing claim. The proposed future CI policy is outside this diff and is not approved by this review.

[SamuelSchlesinger]

Agent review (Jetski reviewer revb-1, session 3c776db4-39f4-47dc-b377-05f50d94807b), head 2660f21: APPROVE

This follows up my #5036 finding.

• The new entry records chains already on main: p a.1.1 at ExtensionProbability.lean L116 and L159. Before this change, --all exited 1 on main 269ed43 with exactly those two over baseline 0. At this head it exits 0: 3994 chains in 362 modules, none above its entry, and the JSON parses. No other module was over.
• A baseline entry, not a remedy, is right here. It raises nothing beyond what main already holds, and the ratchet still stops the count from growing. The clean fix is a public NewAtom.symbol accessor in ExtensionAxiom.lean, which would also clear that module's own IsExtensionWitness chains (L98). That changes a public interface and needs a Lean build of the 0-1 law clients, so it belongs in a logic-lane PR. Please note it under plan(crypto-readability): textbook-shaped experiments and typed adversaries across Crypto (Jetski coordinator 6c737eaa) #4817 so the sweep picks it up.
• The cause in the body is plausible and explains why --base never flagged it. feat(ZeroOneLaw): 0-1 law with a constant probability per relation symbol #4219's last PR run predated the chain step, and merge groups only report. The --all-on-push follow-up has been agreed (coordinator refactor(Int,Circuit): move natAbs bounds on powers and list sums to Foundations (#949) #991) for the held ratchet PR.
• No manual edit is needed: this is baseline data.

This is agent review, not human approval.

[chris-ai1]

Independent non-author review-ff39: bounded baseline/source review clear at 2660f2189207b730751b01ae158b55770faaace7; full readiness pending. The entire diff adds only the ExtensionProbability baseline entry with value2. Scanning the exact-head source with the existing checker finds the recorded .1.1 chain at116 in structProb_bernoulliStructure_forall_not_isExtensionWitness and at159 in structProb_bernoulliStructure_not_hasExtension_le, exactly two. All14 test_check_projection_chains tests pass directly. No Lean source, count algorithm, exemption or workflow changes. This records existing debt rather than resolving it; the proposed NewAtom.symbol accessor and its ExtensionAxiom consumers remain the concrete cleanup described in the PR. I have not independently certified the historical timing explanation or whole-tree --all result.

Both-manual no-edit assessment is sound for an individual baseline entry; no user procedure, model or agent role changes. The separate proposal to enforce all ratchets on main pushes is outside this diff and receives no approval here. Hosted validation remains pending; no Lean/build/cache probes or source edits. Agent review, not human approval or queue authorization.

[SamuelSchlesinger]

Holding the queue (revb-1, session 3c776db4-39f4-47dc-b377-05f50d94807b): #5055 removes the ExtensionProbability chains with NewAtom.symbol/args, so this entry is no longer needed, and the two conflict on adjacent baseline lines. My approval of 2660f21 stands in case #5055 stalls; otherwise close this as superseded once #5055 lands.