[amaybaum]

Draft. Serialized unit 3, authorized by the owner on 2026-11-02 (#924 Option A). Not for merge without the owner's exact-SHA approval.

This PR implements the reviewed M1+M2 correction proposal recorded on #924 (summary comment 6567820151; proposal sha256 prefix 5aef407b3ede43e2; review and confirmation 1fee6d45ca99dc56) as one indivisible unit. It is based on main 7a4321c5. Since the proposal's base 02009693, main has changed only by #1017's audit files. All 15 Main spans and the probe span were re-verified to occur exactly once before editing.

What changes

• papers/Main.md: 15 spans.
  • The imported Barandes result is stated as the source gives it: a separate unitary Ũ(t←0) for each target time, on one space of dimension ≤ n³, with no fixed generator.
  • A fixed Ĥ appears only as OI's in-house form (Q2), at integer horizon times.
  • The n² vs n³ contrast at :216, which the source does not make, is removed.
  • A per-time n² family is recorded as an in-house derivation on paper from Main's one-step Lemma (:212). It is not kernel-certified.
  • At :356 and :658, a failure of the correspondence no longer "costs the compressed form". The ≤ n³ bound stays attributed to its source.
• tdilate_probes.py:73: print-line wording only.
• verification/coverage/LEDGER.json: MAIN:D-unitarily-evolving-qm changes c1bc7b35a7c12e99 → 139a68c2f2c5c3d1, the value computed by proof_census.py. This is the only row that moves.
• sc42: the Main:216 anchor is re-cut, and the controls, result and intended-sites JSONs are regenerated. Each changes only its anchor or site-table hash.
• Main.tex / Main.pdf: rebuilt with sh ./build.sh Main on the native toolchain. The PDF is 99 pages before and after, with no dropped glyphs, and is not provisional.

What does not change

• No theorem or lemma statement, and no new physical assumption.
• No status is promoted, and no physically sourced dynamics is claimed.
• #924 correction (stage 1): Barandes citation labels (M3) and Explainer class statement (M4) #1026's M3/M4 edits are not replayed.
• The optional Bar26 reference is not added.
• No Explainer, book, FULL or other-paper text changes; none restates the import.

Local checks (writer):

• architecture checker: 0 violations; exemptions unchanged (Main 11 → 11, corpus 46 → 46);
• coverage_check: OK, 134 statements;
• check_sc42_integration.py: 618 checks pass;
• mirror, citation and Lean-census checks: pass;
• py_compile and the touched probe: pass;
• register, caps and history scan of the added lines: 0 hits;
• corpus re-grep: no stale fixed-Ĥ or "≤ n³-bounded" attribution remains.

Still to do before the owner's decision: independent exact-head review, and CI including the Lean checks. The five holds (#1009, #1023, #1011, #1003, #918) are unchanged.

---

Generated by Claude Code

[amaybaum]

Serialized unit 3 checkpoint (2026-11-02): head 33211077a28acc71113253e09cbfd6db166a78d6. Awaiting the owner's exact-SHA merge decision; not merged.

Independent exact-head review: READY-WITH-NITS (no blocker).

• Fidelity: applying the reviewed proposal's 15 old→new spans to 7a4321c5:papers/Main.md reproduces the head's Main.md byte for byte, including R2's E1 wording and E10b/E11c. E9 (tdilate_probes.py:73 print line) is the only code change.
• The owner's three distinctions hold: a time-indexed unitary family vs one fixed generator; imported vs in-house; representability vs physically sourced dynamics.
  • No theorem or lemma statement changes.
  • The only census change is the Definition, which becomes weaker.
  • The per-time n² derivation is plain text after the Lemma's proof, with no kernel claim.
• Derived artifacts:
  • The regenerated Main.tex matches the committed file except for its source-sha line, which matches the head.
  • Main.pdf is updated: 99 pages, no dropped glyphs, native toolchain.
  • The single LEDGER row equals proof_census.py --json at the head.
  • The three sc42 files differ only in the anchor and hash; check_sc42_integration.py passes.
  • Architecture checker: 0 violations. coverage_check: OK.
• Mergeability: the parent is main 7a4321c5, and git merge-tree is clean.

Non-blocking nits, outside the authorized scope and left untouched:

1. Four sites still say the import is kept "for compression": Main:536 and :708, GR:20, SM:14. The proposal left these to the owner, and GR:20 is covered by no other issue.
2. Main:218 (Correction planning: scientific overclaims and status corrections (from the 2026-11-01 disposition) #1028's site) now reads inconsistently with E1/E10b and should be handled in Correction planning: scientific overclaims and status corrections (from the 2026-11-01 disposition) #1028's unit.
3. Main:356 carries older "earlier versions" wording that predates this PR.
4. Optional: E1 has no explicit status word.

CI: run 41395967646 (pull_request, verify) passed, with 25 jobs succeeding and 1 skipped as expected. This includes the Lean kernel check and the Mathlib bridge. GitHub reports the PR as mergeable with state clean.

The five holds and every other backlog item are untouched.

---

Generated by Claude Code

[amaybaum]

Merge record. Merged at the owner-approved exact SHA 33211077a28acc71113253e09cbfd6db166a78d6 as a normal merge commit. Immediately before merging, the head still matched the approved SHA and all 26 check runs were green (25 succeeded, 1 skipped as expected).

• Merge commit: c287a57720a94ab160673ba9ef1c76b73e16f1f6. Its parents are 7a4321c5 (main) and 33211077 (the approved head). Its tree is identical to the approved head's tree. It brings the 8 planned files into main.
• Post-merge CI: push CI run 41397348303 on c287a577 passed (25 jobs succeeded, 1 skipped as expected), including the Lean kernel and Mathlib bridge.

The four non-blocking nits are recorded as follow-up obligations on #924 and #1028 (GR:20 is assigned to #1028). None of them was changed by this merge.

---

Generated by Claude Code