[amaybaum]

Draft. Not for automatic merge. Unit 2 of the closure programme for Issue #941. Base: main at 424f28b1e7b1201e9a13bd0e608e1b0e4ad9f93b. Head: 16850df6c03e5c3d350fc3c5308b56b6fd3517d6 (two commits: 087c9e0d68f8a8ae4e3722462770913cded24e2d, the reviewed head, and 16850df6, the review delta; see "Delta after the exact-head review"). Writer: writer-941.

Authority. Owner rulings on #941, comment 6677500012 (amaybaum, Claude Code session chat, 2026-11-06; summary record #1031 c.6677496553):

• item 1: "Approve three separately justified provenance narrowings. Do not land superseded Introduction blobs merely to cure historical references."
• item 2: "Approve correcting the inventory to 29 declarations, including c3_necessity_via_hidden, in both identified READMEs. Preserve evidence bytes."
• "Unit 2 may prepare its documentary PR containing the three SC narrowings, README corrections and retained ledger. Require independent review of the actual 190-row artifact before merging it."
• "Do not merge any of these PRs automatically. Each needs exact-head review, green CI and an owner merge decision."

Not done here, and not authorized: merge, workflow dispatch, any Introduction edit, any change to evidence bytes, any other manuscript edit, Issue closure, board moves.

Edits, mapped to ledger rows and ruling items

File	Lines (base)	Change	Ledger row	Ruling item
verification/audits/manuscript/intro-corpus-audit-20261026/tracks/SC17-explainer-bell/README.md	68–70	three sentences on the draft Introduction at bace5ef8 → two-sentence provenance statement	SC17-68	1
…/tracks/SC31-period-growth/README.md	140–141	two sentences on the draft at 72014a79 → provenance statement	SC31-140	1
…/tracks/SC33-bell-main-book/README.md	111–114	four sentences on the draft at 3e600003 → provenance statement	SC33-111	1
papers/introduction_repro/README.md	4, 68, +row after 85	"28" → "29" twice; add the OIBridge.C3.c3_necessity_via_hidden row	README-28	2
README.md	117	"28 baseline declarations" → "29 baseline declarations"	README-28	2
verification/audits/manuscript/intro-corpus-audit-20261026/CLOSURE-LEDGER.md	new, 519 lines	the 190-row closure ledger	all rows	Unit 2 clause

Diff: 6 files, +529 / −12. The JSON reports are untouched (git diff --stat -- '*.json' is empty; papers/introduction_repro/results-121598983127.json stays blob 61cfd6ea2df4590cc2ff86f90fc8f50ab71201f7).

The narrowed sentence, the same at all three sites with the commit changed:

A side check read the then-draft Introduction (papers/Introduction.md on draft/oi-introductory-paper-20261025 at <commit>, #918; not on main). It is recorded as provenance only: no correction or claim of this record rests on it.

Delta after the exact-head review (087c9e0d..16850df6)

The independent exact-head review of 087c9e0d returned ACCEPT WITH CHANGES (non-material only). One new commit, 16850df6c03e5c3d350fc3c5308b56b6fd3517d6, touches CLOSURE-LEDGER.md only (+15 / −13). There was no force-push and no amend. No status or proposed-outcome cell changed. There are 190 rows; status counts are unchanged (complete 48, superseded 58, transferred 23, duplicate-of 21, not #941 4, open 36).

Each change was verified first-hand at 424f28b1 before writing.

From the review:

1. EV-L note. The recorded acceptance is Audit: the Introduction against the full core OI corpus (gate for #918) #942 c.6433846714; cb2029ce is not on main and is provenance only.
2. Header. One sentence added: the quoted rulings (c.6677500012) govern wherever they select among, narrow or refuse an option offered elsewhere in the ledger. No row was edited for this.
3. R-03. Main:170 → Main:176. Main:176 is the reworded proof line of 3a73cf64; Main:170 is blank.
4. CON-42. "the adjacent remark" → "Remark (two notions of memory), Main:628". Main:628 states "Markov implies P-divisible".
5. X-2. The FINDINGS :660 citation is marked as provenance at 16fc745d (not on main), to be checked in Unit 4 against BH-01 REPORT.md on main. The header's "no row's disposition rests on their content" now names this exception.
6. Introduction line count. "281 lines (the last is \endgroup)". wc -l gives 281, and the file ends with \endgroup\n.
7. rF-25. The key range is "[Main] to [Wei89]", the 43 keys in reference-list order.
8. This PR body. The comment-id count is updated: 54 at the reviewed head, 55 after the SC-30 citation was added.

From the independent Unit 3/4 consistency check (factual cells only):
9. SC-30.

• Added the missing destination Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 orphan 34. It covers ch01:265 (now :271, "burned and replaced"), ch19:248 and Computation:138, which Source-correction gate: every substantive audit finding gets a source fix or a recorded no-change reason #946 c.6442678234 (amaybaum, 2026-10-27) added to SC-30. Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029's body "### 34 — Book and Computation pointers" lists all three. Source-correction gate: every substantive audit finding gets a source fix or a recorded no-change reason #946 c.6442678234 is added to the source cell and Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 orphan 34 to the home cell.
• D-16, D-22, D-24 and D-25 are recorded as "no recorded destination; the finding's quoted wording does not appear at 721f35fb; not adjudicated under Introduction full-corpus scientific consistency audit (gate for #918) #941", replacing "the defect is absent". The current wordings were re-checked:
  • Main:131 "requires only bijective dynamics (Lemma 3) and a non-permutation one-step matrix $T$, under the uniform hidden prior that defines $T$";
  • Main:342 "(C2-slow)";
  • SM:112 "not a statement about accessible windows";
  • GR has 0 hits for "decoupling the sectors entirely".
• The "Genuinely without a home and still present: none" claim is removed. The count-summary bullet and decision-list item 15 are corrected to match.

10. OD-4. The row now names the two sets of families separately; the census statuses were read from verification/lean-manuscript-census.json:
    • OD-4's families (recurrence horizon; physical C4 discharge and round 2; rooted classification) are current.
    • Introduction: reader-focused rewrite (draft for review) #1134 F-1–F-4 are Independent review and census disposition of the four kernel-only Lean families the Introduction cites #1118's four (TrajectoryMemory, FullFutureMemory, RecordFibreIdentification, RootedRecurrenceBridge). They are kernel-only and are not cited by the text (Introduction: reader-focused rewrite (draft for review) #1134 body: "nothing to relabel").
    • Census registration stays with Independent review and census disposition of the four kernel-only Lean families the Introduction cites #1118 under D10 (Independent review and census disposition of the four kernel-only Lean families the Introduction cites #1118 open).

Recorded for Unit 6 (findings of the consistency check, left unapplied here because they would change outcome cells or need Unit 6 confirmation):

• Whole-framework scientific audit of OI: soundness, physical justification and explanatory power #944 legs. S9-I3, S9-I4 and S9-I5 are proposed for relabelling from outcome (a) to (b) on the Introduction side.
• S9-I7. The check did not confirm no-change: L97 states t ≪ t_R as fact. A one-word hedge is proposed, and it needs authorization beyond rulings 4 and 9.
• CON-42. The check confirms (b): the full finding is addressed, and no transfer is needed.
• S9-I2. The check confirms (b).

Checks on 16850df6:

• Release gate: 21/22 PASS; lean-axioms is skipped because there is no local lake, as on main.
• Added-line scan.
  • Delta vs 087c9e0d: 1 caps hit (FINDINGS, a file name).
  • Whole diff vs base: 15 caps hits (file names and acronyms) and 2 history hits ("no longer" in audit rows); local-path, secret, register and model-id 0 each.
• Ledger structure.
  • A cell-by-cell comparison with 087c9e0d changes only these cells: R-03, OD-4, SC-30 (source, applies, home), CON-42 (resolution), rF-25 and X-2.
  • 190 rows with unchanged IDs and order.
• Push triggers: re-inspected; this is a fast-forward push that touches no path-filtered or governed workflow path.

1. The three narrowings, each justified separately

Common checks, done first-hand at base 424f28b1:

• Not frozen. None of the three READMEs is listed in verification/infrastructure/legacy-records.json, none lies under its 75 closed namespaces, and no V3 receipt names a record directory under intro-corpus-audit-20261026 (the only receipts naming verification/audits/manuscript/ are CC-1, CC-2 and CONSC-2, each for its own round-* directory). The legacy-records and v3-receipts gate steps pass on the head. So each is a mutable record, correctable in place (§A.42 item 6).
• Off main. git merge-base --is-ancestor <commit> 424f28b1 fails for all three commits. Their papers/Introduction.md blobs are 7c5f18b4303c816bcb95eba597d693cb460ad92b (bace5ef8 and 3e600003) and 322f5321369581f9089ac248e503a79fe0265f4d (72014a79). Neither blob is among the 36,592 objects git rev-list --objects 424f28b1 lists (full, non-shallow, non-partial clone), and neither is any of the 11 papers/Introduction.md blobs in main's history. All three commits are held only by draft/oi-introductory-paper-20261025 and research/introduction-recovery-r32-20261028.
• No draft blob is landed (ruling item 1).

Site	What the sentence used	Claims of the record	§A.42 item 8, before → after
SC17:68	It paraphrased the draft at bace5ef8 (Bell ceiling with four hypotheses and ±1 in every run; the either/or, ontic parameter dependence and H-Bell; no pre-setting-record, selector or center-independence claim). Nothing else in the file mentions the Introduction (grep).	The track corrects Explainer Bell summaries, the selector paragraph and the center-independence chain. Its stated anchors are Main §3.3 (Theorem, Bell ceiling for a screened local completion, and the either/or) and SM §4.1/§4.3. The Introduction sentence feeds none of the site rows, re-grep counts or follow-ups.	support off main (gap; #918 carrying record #941 c.6666760529 §2) → provenance
SC31:140	It paraphrased the draft at 72014a79 (no recurrence-time number; its :49 and :146 define L as the order of φ). It sits after "Owner decisions" and is the file's only Introduction mention.	The track corrects the recurrence-period statements in ch18 §18.7 and related sites, anchored on	S
SC33:111	It paraphrased the draft at 3e600003 (ceiling at L254; either/or and adopted branch at L258; H-Bell at L258, L260; no outcome-independence placement; "the L306 entry … is proved on paper"). It is the file's only Introduction mention.	The track carries the Main and book part of the SC-17 class. Its anchor is Main §3.3 and its hypotheses (i)–(iv); its site rows and re-grep table are about Main and the book.	support off main (gap) → provenance

In each case the narrowed text states only that a side check read a named draft, that it is not on main, and that nothing in the record rests on it. No claim about that draft's content survives, so no support off main remains.

2. README inventory: 28 → 29

• Missing declaration. Appendix A of the Introduction at f5efa7a0 (an ancestor of main) lists c3_necessity_via_hidden at :356 ("C3Necessity:80, :88, :117"). An independent script read Appendix A's baseline bullets, less the four additional-module bullets (TrajectoryMemory, FullFutureMemory, RecordFibreIdentification, RootedRecurrenceBridge). It found 29 names, equal to the 29 table names after this change, with an empty symmetric difference.
• The added row is sourced from evidence already on main. The JSON report expected.modules["OIBridge/C3Necessity.lean"].reports has {"name": "OIBridge.C3.c3_necessity_via_hidden", "line": 141, "axioms": ["propext", "Classical.choice", "Quot.sound"]} (JSON :162). git show 17b830bc:verification/lean-mathlib/OIBridge/C3Necessity.lean has theorem c3_necessity_via_hidden at :88 and #print axioms c3_necessity_via_hidden at :141.
• All 29 rows checked. The same script checked each row's module, print line and axioms against the JSON, and its declaration line against the source at 17b830bc. There were 0 mismatches.
• Unchanged text. "28-module" (EXPECTED_28, a module count) is unchanged in papers/introduction_repro/README.md:7, introduction-repro-ext/README.md:1, :3 and evidence-replay.yml:18, :22. "Each has exactly one report" and "286 reports" stay true. Row order follows Appendix A (after c3_necessity).

Re-grep after the change (§A.25 step 6). Phrases searched: "28 baseline", "28 declarations", "28 declaration(s) of Appendix", "twenty-eight baseline/declarations". The search covered all tracked text files, papers/, book/ and FULL included. Two hits survive, both legitimate:

• CLOSURE-LEDGER.md:235, the README-28 row, which quotes the defect as it stood;
• verification/programmes/oi-qm/track-b/act-15-pq3d-cancellation-fork/result.md:125, "The 28 declarations whose statement mentions readback", which is a different count.

"29 baseline declarations" or "29 declarations" now occurs at README.md:117, papers/introduction_repro/README.md:4 and :68, and in the ledger. No book, FULL or paper text carried the count.

3. The retained ledger

• Placement (§A.36). The file is verification/audits/manuscript/intro-corpus-audit-20261026/CLOSURE-LEDGER.md. That is the audit directory of the Introduction corpus audit that Introduction full-corpus scientific consistency audit (gate for #918) #941 carries; its tracks/ and introduction-repro-ext/ already live there. It is not at the verification/ root, and artifact-placement and manifest-drift pass.
• Content kept. All 190 rows are kept (sections 1–10: 8 + 41 + 15 + 26 + 19 + 21 + 25 + 10 + 20 + 5). A script compared every cell with the reviewed ledger: the only changed cells are 34 "Owner decision" cells and 2 "Applies now?" cells (README-28, EV-L). Status counts are unchanged: complete 48, superseded 58, transferred 23, duplicate-of 21, not Introduction full-corpus scientific consistency audit (gate for #918) #941 4, open 36. No status or proposed outcome changed. Rows pending Units 3–6 stay pending.
• Converted for main.
  • The header is rewritten: scratchpad file paths and the version-file references are removed. The review and delta check are cited by their Introduction full-corpus scientific consistency audit (gate for #918) #941 records (c.6677061224, c.6677206437) as provenance.
  • "read from local objects" becomes "not on main".
  • An "Off-main objects" paragraph names every unreachable commit and blob the ledger cites, with its role.
  • A line records that git diff 721f35fb 424f28b1 is empty for every cited path, so the line references hold at the base.
  • README-28's "LEDGER-REVIEW finding 3" becomes the Introduction full-corpus scientific consistency audit (gate for #918) #941 record, with the main-checkable basis added.
  • EV-L's "Independently accepted" becomes "Recorded as accepted", with cb2029ce and the re-review file marked off main.
• Owner rulings. A new section quotes c.6677500012 verbatim (the quote was extracted programmatically from the comment), with author and time. It maps each item to the rows it bears on. Each of those 34 rows' "Owner decision" cell gets "; ruled: item N (c.6677500012)" appended, and the cell's original text is kept.

4. §A.42 item 8: every off-main reference in the changed files

Every hex id in the ledger was resolved with git cat-file -t and git merge-base --is-ancestor … 424f28b1. On main (ancestors, or blobs in a reachable tree): 024a2126, 0585dd0d, 0da40cff, 17b830bc, 20ca05fe, 2624d49(c), 2714278a, 3a73cf64, 4759d27b, 51eb9698, 53a3eb3d, 55e3217b, 64a84b12, 6bc2c4af, 6e219231, 721f35fb, 8418ec34, 9020bfa0, 9f9dbc28, a1f1cb0d, a5168789, b64919cd, bdcbd32, c95f2f9e, d9f0a845, f5efa7a0, and blob 61cfd6ea.

Reference (off main)	Where cited	Claim it is attached to	Classification
bace5ef8, 72014a79, 3e600003; blobs 7c5f18b4, 322f5321	SC17:68, SC31:140, SC33:111 (narrowed); ledger SC rows, decision list	after narrowing, that a side check read the draft; ledger: that the gap exists	provenance (the claims use the objects' identity and reachability, not their content)
16fc745d and its files (FINDINGS.md F:n, PLAN.md, CORRECTIONS-LEDGER.md, EVIDENCE.md, proofs/README.md, Track C, FA slices); branch audit/intro-corpus-20261026	"Exact source" column, sections 2–6 headers	where each obligation was raised. Each row restates the obligation, and its disposition ("Applies now?") is checked against main text	provenance
4a260ca9, 44236326 (pre-rewrite Introduction heads; round record …/round-20261104/README.md)	section 2 and 9 headers, rF-07, EV-L	the origin of the R-, rF- and EV-L obligations	provenance
021850d9, a2be1e45	NEW-3b	pins in the old draft text; the row's claim is that the current Introduction cites no pins (main)	provenance
8f6ea594..2bc65ae9, cb2029ce, review/EVIDENCE-RECHECK-2bc65ae9.md	EV-L	the record that step 7 was accepted. The row's (b) rests on #942 c.6433846714 and on #1134's supersession (on main); the row now marks these objects "not on main, provenance"	provenance (narrowed wording)
Branches draft/oi-introductory-paper-20261025, staging/…, corpus/…	SC sites; ledger	object locations	provenance
Issue/PR comments (c.N, 55 distinct ids at 16850df6: 54 at 087c9e0d, plus #946 c.6442678234 added for SC-30; all resolve) and Issue/PR numbers	throughout	planning facts: homes, transfers, owner rulings, review outcomes. These are §A.45 planning-record claims, and the Issues govern them (§A.45 rule 1). The ledger establishes no scientific claim, and this is stated in its header	planning record; provenance for any scientific status. The rulings that settle Unit 2–6 routes are quoted with author and time
Proposed (b) rows whose evidence is a check recorded only in a comment (for example O-26 DOI resolution #942 c.6434035598; R-14/R-19/OD-8 source reads; SC-30 "appears corrected, not independently reviewed")	rows O-26, R-14, R-19, OD-8, SC-30	proposals, not established outcomes. Each stays open or pending Unit 3, 5 or 6 confirmation, and the rulings (items 7, 8, 15) require fresh checks	support off main for a proposal, not presented as established (§A.46 item 3). These are carried open by their rows, not closed here
Unit 1 review files (not published)	header, README-28, count summary	that the review and delta check returned their verdicts	provenance, cited by their #941 records c.6677061224 and c.6677206437

Result: no unclosed gap in a claim this PR presents as established. The three SC gaps are closed by narrowing. Ruling item 1 bars landing the blobs.

5. Checks run (local, §A.40; no Lean build, no dispatch)

• Release gate. python3 tools/release_gate.py on the head: 21 of 22 steps PASS. These include artifact-placement, manifest-drift, voice, voice-scope, claims, duplicate, mirror, citation, coverage, lean-manuscript, legacy-records (303 records in 75 closed namespaces intact), v3-self-test, v3-corpus and v3-receipts (53 hold). lean-axioms fails only because lake is absent locally ("SKIPPED - no lake on PATH"); it fails identically on main at 424f28b1.

• SC42 checker. check_sc42.py cannot run on the current tree: it reads papers/Explainer.md, which no longer exists on main. Its section-[5] added-text regexes (register, revision voice, caps, secrets, local paths) were run on this diff, together with a model-identifier pattern. Results:

  • local-path 0, secret 0, register 0, model-id 0;
  • caps: 14 hits, all file names or acronyms (README, JSON, FULL, FINDINGS, CORRECTIONS-LEDGER);
  • history: 2 hits, "no longer" inside ledger rows that describe audit status in an audit record (§A.33 governs papers/ only; SC42 exempts README records).

• Other checks.

  • The 29-row consistency script described in §2.
  • A row-by-row cell comparison of the ledger against the reviewed ledger (190/190 rows; only the cells listed in §3 differ).
  • The ruling quote is byte-identical to the comment's quoted block.

• Trigger check (§A.43 item 4). push-triggered workflows were checked before pushing:

  • verify.yml and hidden-sector-replay.yml trigger on pushes to main only;
  • bg2-orientation-design.yml and bridge-compatibility-research.yml are path-filtered to paths this diff does not touch;
  • evidence-replay.yml, oret-phasea.yml, pe01-bounded-tests.yml and project-board.yml are dispatch-only.

  The push started no governed launch. This PR triggers only ordinary verify.yml pull-request CI.

Review requested

The independent exact-head review of the 190-row CLOSURE-LEDGER.md at 087c9e0d returned ACCEPT WITH CHANGES (non-material); its findings are applied in 16850df6. A delta check of 16850df6 is requested. The review confirmed O-17 and O-23 (G1 §4) against Introduction L203 and L205. Then green CI and an owner merge decision. This PR is for #941 and does not settle the Issue: EV-28 remains the hard closure condition.

https://claude.ai/code/session_011zDyUSyEszk3JJx83uXKKq

---

Generated by Claude Code

[amaybaum]

Record of the independent reviews of #1159. Posted after the merge. The #941 Unit 6 audit found that both verdicts had been relayed only in the coordinator's summary (#941 c.6677992216) and in the reviewer's working file. This comment restates them; it changes nothing.

1. Exact-head review at 087c9e0d68f8a8ae4e3722462770913cded24e2d: ACCEPT WITH CHANGES, all findings non-material. The reviewer is a separate agent that wrote neither the ledger nor this PR. The review was read-only.

• Scope. Exactly 6 files. The evidence JSON is unchanged (blob 61cfd6ea…).
• SC17, SC31, SC33. The drafts each one cited are not reachable from main. No correction or claim in those tracks rests on them, and the records are not frozen.
• The 29 declarations. Appendix A at f5efa7a0, less its four additional-module bullets, lists 29 names. They match the 29 README rows in order. Every row matches the JSON and the Lean source at 17b830bc, and the added c3_necessity_via_hidden row is correct.
• The 190-row ledger. The row counts per section and the status counts match the reviewed scratch version. All 36 changed cells are accounted for, and no status or outcome cell changed. The owner ruling is quoted byte-identically. 45 sampled rows are accurate apart from small line errors. O-17 and O-23 were confirmed against the Introduction.
• References off main. Every git id resolves, and all 54 comment ids resolve.
• Leaks and keywords. No local paths, secrets or model identifiers, and no closing keywords.
• CI. 25 checks succeeded, 1 was skipped, and none failed.
• Findings. Eight non-material findings: an EV-L wording fix, a header sentence saying the rulings govern, R-03 → Main:176, CON-42 → Main:628, X-2 provenance, the line count, the key range, and the comment-id count in the PR body.

2. Delta review of 087c9e0d..16850df6c03e5c3d350fc3c5308b56b6fd3517d6: ACCEPT, with no material findings.

• Findings 1–8 were applied correctly.
• The SC-30 and OD-4 cell corrections were verified against Source-correction gate: every substantive audit finding gets a source fix or a recorded no-change reason #946 c.6442678234, Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 (orphan 34), the census at 424f28b1, and Independent review and census disposition of the four kernel-only Lean families the Introduction cites #1118.
• No status or outcome cell changed: 190 rows, with status counts 48/58/23/21/4/36.
• The comment-id count is 55.
• Exact-head CI run 42170512570 succeeded: 25 checks passed and 1 was skipped.
• Two cosmetic leftovers remained in the SC-30 owner-decision cell wording and in the PR body. Neither blocked the merge.

The owner approved the merge at 16850df6 (#1031 c.6678672357). It landed as 374b2ef3; the merge record is #941 c.6678793390.

---

Generated by Claude Code