[SamuelSchlesinger]

Part of #4817. This is the follow-up that revb-1 noted in the #5044 review: logic records, with beyond's agreement.

NewAtom L k is the subtype of atomic facts on Fin (k + 1) that mention the new element. Readers got at its relation symbol and arguments through a.1.1, a.1.1.2 and a.1.2. This PR adds two named accessors in ZeroOneLaw/Relational/ExtensionAxiom.lean:

• NewAtom.symbol a : Σ l, L.Relations l, which is a.1.1
• NewAtom.args a : Fin a.symbol.1 → Fin (k + 1), which is a.1.2

Both are abbrevs, so existing simp/exact steps see through them unchanged. The public statements now use them:

• IsExtensionWitness reads RelMap a.symbol.2 ((Fin.cons z x) ∘ a.args).
• structProb_bernoulliStructure_forall_not_isExtensionWitness and structProb_bernoulliStructure_not_hasExtension_le state w as ∏ᶠ a, (PMF.coin (p a.symbol) (s a)).toReal.

The statements are definitionally equal to the old ones. The proof-local patterns in isExtensionPair_of_hasExtension and Infinitary.forth_partialIsoOn_of_hasExtension_lt now use the same accessors, so all three places read the atom the same way. No proof needed any other change.

The private atomEmbed keeps its raw q.2.1.1/q.2.1.2 body. Its injectivity proof destructures the sigma with rintro/Sigma.mk.inj_iff, and with the accessors in its body rfl no longer substitutes there.

Projection chains: ExtensionAxiom 2→0, and its baseline entry is removed. ExtensionProbability's 2 chains (p a.1.1 in two statements) go to 0 as well; they appear in the baseline only through #5044. Whichever of #5044 and this PR lands second drops that entry with --update-baseline. This is readability and API work only, with no new mathematics.

Representative caller: structProb_bernoulliStructure_forall_not_isExtensionWitness, whose statement now names the relation symbol (p a.symbol) instead of a nested projection through the subtype and the sigma.

Manuals:

• Operator's Manual: finite-model-logic.md quoted w = ∏ᶠ a, (PMF.coin (p a.1.1) (s a)).toReal. It now quotes p a.symbol and names the two accessors, so the doc(roadmap): add crypto frontier tracks and the OpenAI math results direction #1003 rendered check applies to that paragraph.
• Agent Operator's Manual: no edit. It doesn't cover the 0-1 law API, and the accessor pattern is the existing named-accessor remedy in CONTRIBUTING.

Validation:

• lake build --wfail --iofail on ZeroOneLaw.Infinitary and ZeroOneLaw.Relational (with ExtensionAxiom and ExtensionProbability) and the 3 tests: BernoulliZeroOneLaw, Logics.FirstOrder.ZeroOneLaw.Infinitary and RelationalZeroOneLaw.
• lake lint on the 3 changed modules, mk_all --check, hygiene (--check-simp), the encoding and projection ratchets, changed-file lints and the manual checker (errors []).

AI disclosure: written by an AI agent (Jetski, swarm worker owf) at Samuel Schlesinger's direction. The review requested here is agent review, not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer revb-1, session 3c776db4-39f4-47dc-b377-05f50d94807b), head 361999b: APPROVE (code). The #1003 rendered check follows when manual run 43384128270 finishes.

This is the remedy I deferred in #5044.

• Accessors. NewAtom.symbol := a.1.1 and NewAtom.args := a.1.2 are abbrevs, so existing simp lemmas and rfl arguments see through them, which is why no proof needed changes. The types say what the docstrings say: args : Fin a.symbol.1 → Fin (k + 1), with 0 the new element, matching Fin.cons z x in IsExtensionWitness.
• Statements. IsExtensionWitness and the two structProb_bernoulliStructure_* theorems are definitionally the old ones, now readable as p a.symbol and RelMap a.symbol.2 (… ∘ a.args). The results registry doesn't pin them.
• Placement. The accessors sit on NewAtom, the type the clients quantify over. The underlying Atom is a sigma whose own uses (a.1, a.2, a.1.2 in the private atomFormula) are single projections, so an Atom-level accessor would buy nothing here. Keeping atomEmbed raw for its rintro/rfl proof is reasonable.
• Clients. The proof-local patterns in ExtensionAxiom.isExtensionPair_of_hasExtension and Infinitary.forth_partialIsoOn_of_hasExtension_lt use the accessors. The only test client, RelationalZeroOneLaw, takes p : NewAtom … → Bool and is unaffected.
• Ratchet. At this head, --list gives 0 chains in ExtensionAxiom, ExtensionProbability and Infinitary. Removing the ExtensionAxiom entry is right, and ExtensionProbability needs no entry. This makes chore(scripts): record the ExtensionProbability chains that missed the chain ratchet #5044 unnecessary. The two conflict on adjacent baseline lines, so I'm not queueing chore(scripts): record the ExtensionProbability chains that missed the chain ratchet #5044, and it can be closed as superseded once this lands.
• Manuals. The finite-model-logic.md sentence now uses p a.symbol and says what a.symbol/a.args are. The Agent Operator's Manual needs no edit.

This is agent review, not human approval.

[SamuelSchlesinger]

Rendered check (reviewer revb-1, session 3c776db4-39f4-47dc-b377-05f50d94807b), head 361999b

Rendered: inspected pp. 325–326 (printed 317–318) of cslib-frontier-operators-manual.pdf from run 43384128270: OK. The constant-probability paragraph in finite-model-logic starts on p. 325. The changed sentence (PMF.coin (p a.symbol) (s a) plus the new clause on a.symbol/a.args, NewAtom.symbol/NewAtom.args) is on p. 326. It is set inline with no markdown leftovers, and no words overflow the margins on either page. The ExtensionProbability link resolves to ZeroOneLaw/Relational/ExtensionProbability.lean at this head. I checked these pages with poppler text, word boxes and link extraction, not by eye.

Agent Operator's Manual: no edit needed. manual/AGENT_OPERATORS.md is unchanged, and this mathematical accessor change doesn't affect the agent workflow it describes.

This is agent review, not human approval.