[amaybaum]

These are the Main.md precision edits held out of #922 (merged as 8dc36d55). The branch is reconciled with main by a merge commit, which keeps the reviewed history.

• Head: 75a9944487b8b415bd40b5b9002c79650c6f8fde, tree cf5d29cc.
• Files changed: papers/Main.md, papers/Methodology.md (one mirror line), verification/coverage/LEDGER.json, and their regenerated .tex and PDFs.

Merge: authorized by the owner at exact head 75a99444, as a normal merge commit.

Changes

Commit	Site	Change
607c23e7 B-F3	Main:16, :530	The Q_fb class is stated as the kernel defines it.
d2a7c4ff B-F4	Main:28	The introduction states the identification at its proved scope.
6909c672 B-F5	Main:608, :690	The characterization's status is stated at its proved strength. No OIBridge module formalizes (ii)⟺(iii).
510df1d1 B-F6	Main:580	Summary claim (2) is stated with its proof route.
0a172590 B-F10 + eb3e5fc5	Main:62, Methodology:146	Double stochasticity of uniform-prior marginals is attributed to counting, not to Birkhoff–von Neumann (the converse direction).
22625cd2 B-F12	Main:167, LEDGER	The readback lemma states only the hypothesis its proof uses.
deb1c913	merge	main 8dc36d55, carrying #922, merged in. Main.tex regenerated; LEDGER and census reconciled.
045fd344	PDFs	Main.pdf and Methodology.pdf rebuilt.
ec6beb61	Main:580, :588, :532	See below.
1cafacf8	PDF	Main.pdf rebuilt.
a04443bf	Main:86, :522	See below.
2c5d7c30	PDF	Main.pdf rebuilt.
4c5012ab	Main:530, :580	See below.
75a99444	PDF	Main.pdf rebuilt.

ec6beb61

• Main:580 and :588 carry the joint-law formalization caveat of Main §1.5: foundational equivalence S ⟺ D and the S_imp_D statement #922's Main:99. The kernel results in HiddenMemory.lean are stated for a joint law R.w on Hist × V × H.
• Main:532 now reads "initial law diagonal".

a04443bf

• The pointers at Main:86 and :522 now read "(§1.2, Remark on the measure as a realization datum)". The former targets, a "§1.3 Remark" and a "§1.4 Remark", do not exist.
• The LEDGER fingerprint of MAIN:L-partition-relativity-under-canonical-invariant is re-affirmed. Only the pointer text changed.

4c5012ab

• The Q_fb class names the read map ("the visible record a fixed function of each outcome").
• Summary claim (2) carries its status word.

Verification

Independent review: ACCEPT WITH NITS at 2c5d7c30, with the scope addition reviewed on its own as ACCEPT.

• Every changed sentence was checked against its kernel theorem in OIBridge/, both directions named (§A.34).
• Coherence was checked with Main §1.5: foundational equivalence S ⟺ D and the S_imp_D statement #922's §1.5 text and with the Explainer after Explainer: repair the Liouville paragraph; correct the measure-uniqueness statements #919.
• The merge was confirmed to be the exact union of the two sides.
• .tex files rebuild byte-identically at every commit.
• An independent PDF rebuild gives identical text, and the rendered pages are clean.

The two required nits, N1 (the read map) and N2 (the status word), are applied in 4c5012ab in the reviewer's wording. The word diff 2c5d7c30..75a99444 is exactly those two insertions plus the regenerated .tex and PDF.

Checks at the head all pass:

• staleness, voice, claims, duplicate, coverage (128), census, dependency-label --strict;
• mirror, citation (112/0), architecture (259/0);
• legacy_records_check (303 intact);
• edge-rigidity, finite-horizon equivalence and equivalence-chain probes.

Pre-merge integration check on the trial merge with main ebf98d83 (clean, tree c1cc4b57):

• the checks above, plus artifact-placement, build_migration_manifest --check, and the canonical-measure and Bohr-frequency probes;
• legacy records: 303 intact;
• V3 self-test.

All pass. The PR's CI at 75a99444 is green: 25 pass, 1 skipped.

Some commit messages of the original seven say "(local draft, not pushed)", and eb3e5fc5 cites a superseded draft SHA (568d22b7). These are left unchanged so that no history is rewritten.

Optional observations, not applied:

• O1: a (C1)/(C3) "which condition is primitive" remark at Main:608.
• O2: book ch01:159 "hidden register prepared in the corresponding prior" could be harmonized with Main:532, in both files.
• O3: Substratum:94 cites "[Main §2.2]" for an argument in §1.2. This predates the PR.

Related: #922 (merged foundational correction), #924 (F13 ≤ n³ planning), #926 (manuscript consistency for the book, GR and Explainer; leaves Main.md untouched).

🤖 Generated with Claude Code

https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb