[amaybaum]

Draft. Not authorized for merge. This is Option 1b of the owner rulings on K1-RDY (#1031 c.6651204512, amaybaum, 2026-11-05): "Prepare self-contained paper proofs of the blindness lemma, the P1 invariant-measure lemma and L-O(i)/(ii). Have them independently reviewed. Land their support on main through a separately approved, narrowly scoped PR before the new round's base D is established."

Head

1901063504f649bd453d7b5f87add395d6974ec7: one commit on main f5c281ae. It adds two files under verification/programmes/oi-qm/reconstruction/k1-rdy-proofs-20261105/:

• LEMMAS.md: the four written proofs.
• README.md: purpose, status, sources and limits.

The directory is a sibling of #1114's k1-rdy-20261105/. The two PRs do not collide.

Content

Every proof is marked "written proof, not independently reviewed". All are hand derivations: no enumeration, model computation, Lean or workflow.

• Blindness lemma (recovered text lines 97–100): proved as stated.
• P1 invariant-measure lemma: the recovered text names P1 (lines 244–245) and uses its content (lines 72–76), but never states it. LEMMAS.md therefore assembles a statement from those lines and their earlier sources, and labels the assembly as the writer's for the reviewer to check. It is then proved in four parts:
  • (a) for a bijection on a finite set, a measure is invariant exactly when it is a mixture of uniform measures on cycles, with unique weights;
  • (b) the law of the state is the same at every tick;
  • (c) the support is a union of cycles;
  • (d) μ(E_{t_0}=0)=1 exactly when the measure is carried by the cycles on which E vanishes.
• L-O(i) (lines 102–106): proved as stated, each direction separately (§A.34).
• L-O(ii) (lines 102–103, 107–110): proved as stated, each direction of "differs iff ⊊" separately.

No counterexample or gap was found, and no correction is proposed. Three readings are marked as the writer's own:

• the "offset" reading of t in the region rule;
• "determines"/"fixes" read as "constant on the event";
• "the smaller subgroup" read as p(K_O ∩ ker L).

The recovered preregistration

The 313-line recovered text (sha256 a93f3f33f0c5a6e8b2467312d184fa2d2e915296490948938c4dd7832c64bb63, on #1114 at e18b36e3) is neither copied nor modified. Statements are quoted verbatim from it; each block quote was checked against it. Its line numbers serve as locators only, because the text is not on main.

Off-main references (provenance only, §A.42 item 8)

• OI ↔ QM equivalence: proof gate (dependency index; carries #885) #914 c.6564008455 (proposal r3) and c.6564018307 (its review).
• K1-RDY: paper-only readiness investigation under fixed selection rule #1031 c.6567537517 and c.6567522034.
• research(#1031 K1-RDY): recovery of the accepted preregistration (WIP / UNVERIFIED; not frozen) #1114 c.6650931698 §3 (draft proofs), and research(#1031 K1-RDY): recovery of the accepted preregistration (WIP / UNVERIFIED; not frozen) #1114 at e18b36e3.

None is offered as support. The proofs are self-contained.

Local checks at the head

legacy_records_check.py (303 records intact), citation_roles_check.py, duplicate_check, staleness_check and artifact_placement_check: exit 0.

Still needed

• Independent proof review of LEMMAS.md at this head. If a lemma fails, the result comes back as a scoped correction for an owner decision.
• CI.
• Separate owner merge approval. Landing must precede the new round's base D.

Not authorized here: F designation, workflow dispatch, enumeration or computation, or a merge.

---

Generated by Claude Code

[amaybaum]

Independent proof review of 1901063504f649bd453d7b5f87add395d6974ec7 (read-only, model-authored, not the writer).

Verdict: ACCEPT WITH CHANGES. All four proofs are correct, with every equivalence proved in each direction (§A.34). The block quotes match the recovered text byte for byte. The recovered text's sha256 a93f3f33…bb63 (313 lines) reproduces, and so do the recorded provenance digests. The changes are wording and locator fixes. No statement or proof step changes.

Result	Verdict	Notes
P1 invariant-measure lemma	VERIFIED WITH CORRECTIONS	The assembled statement is faithful to the uses at P72–76, P236 and P244. Part (d) goes beyond what the text uses and should be labelled so. P74's use (P2's energy-shell measures belong to 𝓘) should be mapped. Optional addition: φ^k(supp μ) = supp μ.
Blindness lemma	VERIFIED WITH CORRECTIONS	Correct under the offset reading of t, which P37–38 force. "Both readings give it" (L55–56) is false as written and needs rewording. The CC-SCOPE application and the (c1) side note are correct. Two locator fixes: r3 lines 76–77; REV-r3 106–107.
L-O(i)	VERIFIED	D10's reading coincides with the measure reading. The "if, in addition" reading is the natural one; marking it is optional.
L-O(ii)	VERIFIED	"The smaller subgroup" = p(K_O ∩ ker L) is the natural reading. Weak readiness is within the text's scope.

Other changes:

• C2: the D8 quote drops "(R1, MR-pre:162)" without marking the omission.
• C3: "quoted verbatim" needs the exception of P1's assembled statement (LEMMAS L15–16; README L27–28).
• C4 (required, §A.42 item 8): state that the quotations are the text's statements only checkably once lines 1–313 are on main.
• Typo: L43, "lines 31–33".

Also checked:

• No overstatement: every section is marked "written proof, not independently reviewed".
• No adoption: nothing is adopted or certified.
• Exclusions listed: the text's uses the package does not prove are named.
• Register: neutral.
• Hygiene at the head: legacy records (303 intact), citation roles, duplicate check and artifact placement all exit 0.

Next: the writer applies these changes, then a delta check and CI. No merge is authorized.

---

Generated by Claude Code

[amaybaum]

Merge record. Owner approval (amaybaum, Claude Code session chat, 2026-11-05):

#1119 K1-RDY | badebef | APPROVED. Execute serially, using normal merge commits: Merge K1-RDY first, after a final head, mergeability and CI check. Verify post-merge main CI is green. […] No new scientific claims or correctness-band promotions are authorized by these merges.

Pre-merge checks (immediately before merging)

• The head was badebefc367a0ce55c588231827fa7b895dbf9ba and main was 53a3eb3d.
• The PR was mergeable and clean.
• On the head, 25 checks passed and 1 was skipped.
• The PR was marked ready for review, then merged with "Create a merge commit" and expectedHeadSha.

Merge

• Merge commit: 4f016afd943f5a3939493eab752664949e90dbbb. Parents: 53a3eb3d (first) and badebefc (second).
• Tree: 42c67a15f866f34dae9e83812aebd271aebcfba0. This is identical to the reviewed head's tree; it adds the two record files, LEMMAS.md and README.md (+410).
• Legacy records: 303 intact.

Post-merge CI. The verify push run 41989036801 on 4f016afd succeeded, with 25 jobs passing and 1 skipped (the matrix placeholder). The Mathlib bridge Build and Release gate both succeeded.

Scope. The written proofs of the blindness lemma, P1 and L-O(i)/(ii) are now on main, ahead of the new round's base D. This merge promotes no claim. No freeze, dispatch, enumeration or round execution follows from it; the next step is the V3 supersession and its amendments, for review.

---

Generated by Claude Code

[amaybaum]

Late posting: the delta check of d8bfd07b. This record is administrative. The independent reviewer (model-authored, read-only) delivered the check to the coordinating session on 2026-11-05, before 6525ad34 was committed (06:53:41Z). It was never posted to GitHub. Under OD-2 (#1114 c.6653656756), the #1119 review must be recorded on main, so the check is posted here now. The reviewer returned the text word for word from its own context; nothing in it was reconstructed or edited. The coordinating session has not changed it either.

----- BEGIN VERBATIM REPORT (delivered earlier on 2026-11-05) -----
Delta check of d8bfd07b against 19010635: ACCEPT WITH TWO SMALL CHANGES. Every requested change is applied accurately and nothing else changed. The two changes are counts that the new additions left out of date. If both are made exactly as below, ACCEPT, with no further review needed.

d8bfd07bf591eeeeb107ef9842547dc53e195bef has the single parent 1901063504f649bd453d7b5f87add395d6974ec7. It changes only LEMMAS.md (+32/−18 together with README) and README.md (2 lines). L-numbers below are lines of LEMMAS.md at d8bfd07b; P-numbers are lines of PREREG-RECOVERED.md at e18b36e3.

Requested changes, each checked in the diff

• P1 (i): applied. L100–101 now asks the reviewer to check "(a)–(c)" and adds "Part (d) is not used by the text (source: r3 line 96); it is proved here as a corollary". The same sentence is in §1.3.
• P1 (ii): applied. §1.3 maps the P2 shell-membership use at P74–75 to (a)'s "if" direction plus ℰ's conservation (SM:294–296), marked as not proved here. §5 item 3 lists it too.
• P1 (iii): applied. (c) now ends "hence φ^k(supp μ) = supp μ for all k ∈ ℤ".
  • The added proof clause ("and so does each φ^k, k ∈ ℤ") is correct and sufficient.
  • The cycle paragraph already shows φ(c) = c and φ^{−1}(c) = c for every cycle c, so every φ^k maps each cycle, and therefore each union of cycles, onto itself.
• C1 (the D4 reading): applied verbatim as I proposed.
• Locators: fixed. r3 is now "76–77" in both the table and §1.1, and REV-r3 is now "106–107".
• C2 (D8 quote): applied. The quote ends "σ′ [...]", followed by the note naming the omitted citation "(R1, MR-pre:162)".
• C3 (P1 is not quoted verbatim): the exception is now stated in LEMMAS.md §0.1 and in README L27–28.
• C4 (§A.42 item 8): the required sentence is in §0.1, verbatim.
• Typo: "lines 31–33" is corrected.
• Optional D10 note: added. It is correct, because both conditioned laws have full support on their events.
• Optional "If, in addition" reading: added in §3.1 and marked (reading), with the O = S counterexample. It is correct.
• Optional L18 reword: applied. It now reads "cited as provenance only; each row below is provenance: …", which is slightly redundant but acceptable.

Remaining changes (both are counts left stale by the additions)

1. LEMMAS.md L86–87 says the text "uses its content at three places", but §1.3 now records a fourth use, P74–75. Either change "three" to "four" and add a bullet — "lines 74–75: "P2's energy-shell measures (SM:294–296) are members"" — or append "; a fourth, lines 74–75, is noted in §1.3" after the list.
2. There are now four marked readings, because "If, in addition" was added. Two places still list three:
   • LEMMAS.md §5 item 2 (L362) names only D4, D10 and "the smaller subgroup". Add "and the reading of "If, in addition" in §3.1".
   • README L22 says "three marked readings". Change it to "four marked readings".

Re-verification

• The text's sha256 at e18b36e3 is a93f3f33…bb63, with 313 lines.
• The block quotes still match byte for byte: L178–181 = P97–100, L238–242 = P102–106 and L293–296 = P107–110.
• Hygiene, run with python3 -I in a detached worktree at d8bfd07b (since removed):
  • legacy_records_check.py d8bfd07b…: exit 0, "303 record(s) in 75 closed namespace(s), all intact".
  • duplicate_check.py: exit 0.

Scratchpad overwrite. During this check, my first-pass scratch copy prereg.md in the shared session scratchpad had been overwritten by another writer: it now holds different content, 699 lines, with sha256 4d0629ec…. It is a scratch file, not a repository file, and no verdict rests on it. I re-extracted the text from git for every check above; my first review's comparisons had already confirmed the correct sha256 before the overwrite. The coordinator may want to know that another process is writing into this scratchpad.

No edits, commits, pushes, posts or dispatches were made.
----- END VERBATIM REPORT -----

New statement by the same reviewer, dated 2026-11-05 and written at posting time (not part of the report above).

• It confirmed read-only, from git diff d8bfd07b 6525ad34, that 6525ad34 (single parent d8bfd07b) applied exactly the two count fixes and nothing else.
• The commit changes only LEMMAS.md (+4/−3) and README.md (+1/−1).
• Item 1: "uses its content at four places", plus the bullet for lines 74–75.
• Item 2: §5 item 2 names all four readings, and README reads "four marked readings".

---

Generated by Claude Code

[amaybaum]

Correction on authorship. This clarifies what two comments on this PR record; it changes no scientific status.

• c.6651717259 (the "review" comment). The coordinating session wrote this comment as a condensed posting of the independent reviewer's report. It is not the reviewer's report verbatim. The reviewer has confirmed that its verdicts and findings match what it delivered: the per-lemma outcomes, items C1–C4, the locators and the hygiene results.
• c.6653737476, the statement after the END marker. The coordinating session condensed this into the third person from a statement the reviewer wrote at posting time. Its substance matches. Only the block between the BEGIN and END markers is the reviewer's report word for word.

---

Generated by Claude Code