[amaybaum]

Summary

This is the guiding draft PR for the scientific consistency audit the owner required before the Introduction (#918) can land. The plan is in verification/audits/manuscript/intro-corpus-audit-20261026/PLAN.md.

• Objects: the Introduction at Introduction paper: reconcile sources and integrate scoped theorem recoveries #918 4a260ca9, and the corpus at main b64919cd.
• Scope: the core physics papers, the book's appendices and physics chapters, the Lean modules, and the verification records. The audit does not assume Main.md holds every proof.
• Method:
  1. proof inventory;
  2. claim-to-proof mapping;
  3. status classification: weakest link, hypotheses carried along, equivalences traced one direction at a time;
  4. cross-paper consistency;
  5. independent review;
  6. a final landing gate on the revised Introduction.

Status

• WIP: the plan is committed, and the inventories come next.
• This PR changes no manuscript text. Corpus corrections it identifies go to the owner as separate proposals.
• Introduction paper: reconcile sources and integrate scoped theorem recoveries #918 stays on hold, and no merge authorization is in effect.

Related

• Tracking Issue for the audit.
• Introduction paper: reconcile sources and integrate scoped theorem recoveries #918, the Introduction.
• AGENTS.md: whole-framework scope for corpus reviews #940, the review-scope rule.

---

Generated by Claude Code

[amaybaum]

Checkpoint 290822b3: step 7 aggregated. Every matrix row now carries an evidence level (WIP; independent review of the evidence layer running)

This session is now #942's writer, at the owner's direction. It continues from the handoff on #941.

What changed

• evidence/scripts/E4_aggregate.py writes evidence.json and renders EVIDENCE.md, the step-7 outputs PLAN.md names. Each of the 409 matrix rows gets an evidence level from the 178 items of E1–E3.
• The rule, which EVIDENCE.md states in full:
  • A kernel link takes the weaker of E1's per-declaration certificate item and coverage item.
  • A file-sourced kernel link takes the items that name its file.
  • A computation link takes E2's items for the row.
  • A row takes its weakest evidence-bearing link.
  • A row with no such link takes its CI-receipt items, where it has any. Otherwise it is traced-only, with the reason stated.
  • Any failed item fails the row.
• merge_matrix.py copies each level into matrix.json. render_matrix.py shows it as a column, with a summary table and a counts control. No other matrix field changed; that was checked row by row.

Result

Evidence level	All rows	Rows with an evidence-bearing link
reproduced	67	58
certificate-checked	153	149
traced-only	187	28
failed	2	2

• Failed: I-054 and I-103. This is E2-10: "exact probes" (L84) and Main's "Certified exactly" are floating point.
• Gaps: each of the 28 evidence-bearing rows left at traced-only is listed with its gap. Most are exact-algebra links that no E2 computation reached.
• Not applied: EVIDENCE.md lists matrix labels that disagree with their own chains, as corrections:
  • four rows whose status implies an artifact that their chain lacks;
  • seven kernel-layer links that cite paper, ledger or roadmap lines.

matrix/scripts/b5_check.py: both gaps E2 found are fixed.

• B.2's I(X0;X2|X1) is computed exactly from the joint law: 1 bit. A countercontrol gives 0 on the independent law, 1 on the copied law and 0 on the constant law.
• The three-hidden-state variant's P(x2=0|x1=1) is computed for general a: a/(2−a), as R-04 states.

Checks: E4_aggregate.py --check and render_matrix.py --check pass. artifact_placement_check passes. legacy_records_check at 290822b3 finds 303 records intact. A scan of the added lines found no sensitive data. No push-triggered workflow matches this path.

Still proposed for owner authorization, not dispatched:

• a fresh-build CI reproduction of introduction_repro at 17b830bc;
• an extended expected result covering the additional modules (OD-15), before their CI logs expire;
• BHa and BHb mutants.py replays.

#918 stays on hold. No merge, dispatch or manuscript change is requested.

---

Generated by Claude Code

[amaybaum]

Checkpoint 818bcd60, step 7 (evidence verification). This commit applies the evidence-layer review (review/EVIDENCE-REVIEW.md, of 290822b3, ACCEPT WITH CHANGES). WIP: a focused independent re-review is running.

Required changes

• R1. CI receipts set a row's level only when the chain is entirely build, CI or records links (I-044, I-308 to I-310, I-312). The nine black-hole physics rows are now traced-only.

• R2. The aggregator now grades each row only on its load-bearing links. The load-bearing set depends on the proof status:

  • proved-kernel: the kernel links;
  • proved-paper, exhaustive-exact, numerical and calibration: all links, with paper and literature steps traced-only;
  • open, conditional, conjecture and unsupported: the row is traced-only.

  Each row also records an artifact level, which shows what its checked artifacts reach.

• R3. Formal-coverage items carry a per-claim not_covered list (E1-92/I-129, E1-98/I-088, E1-99/I-071).

• R4.

  • E2-07 now rests on the BHb checks.py replay.
  • The C1 sweep in E2_bh02.py now evolves dense vectors and computes exact ranks. Its countercontrols fire, and a mutant evolution is caught.
  • The CI proposal now asks only for the -O replay and mutants.py.

• R5.

  • E2-11 is now a fail of L56's tag under L30's definition.
  • E2-10 and E2-11 each state their failure scope: the evidence tag fails, while the bound and the realization stand.

• R6. matrix/chain-relabels.json corrects the kernel-labelled paper, ledger and ROADMAP links. merge_matrix.py applies it and keeps mapper_layer. Theorem 1 (I-063) is now certificate-checked.

• R7. E4_aggregate.py --check and render_matrix.py --check now compare every row's level and basis with evidence.json. A one-row mutation fails both.

Optional changes

• O1: computation items no longer match links that name other records or probes.
• O2: listing gaps closed.
• O3: a matched fail fails the link.
• O4: the limits on log-text axiom reports and fresh elaboration are stated, and E3-14 is reworded to match.
• O5: refuted rows carry counter-evidence.
• O6: E2-19 is retyped as ci-receipt.
• O7: b5_check.py has countercontrols.
• O8: the pipeline order is documented.

Levels (409 rows): 43 reproduced, 130 certificate-checked, 233 traced-only, 3 failed. The failed rows are I-054, I-071 and I-103, all failures of an evidence tag.

Checks: E4_aggregate.py --check and render_matrix.py --check pass. All eight E2_*.py scripts exit 0. artifact_placement_check, and legacy_records_check at 818bcd60, pass. The added-line scan is clean. No push-triggered workflow matches these paths. No dispatch was made.

---

Generated by Claude Code

[amaybaum]

Checkpoint 8f6ea594, step 7. The independent re-check of 818bcd60 returned CHANGES NEEDED; its report is retained as review/EVIDENCE-RECHECK-818bcd60.md. This commit responds to it.

N1, relabels that raised rows. The relabels of I-042, I-052, I-258 and I-281 are dropped. Those links are kernel-proved steps sourced to paper lines that cite the kernel, so they keep the kernel layer and grade traced-only until they are sourced to declarations. I-052 and I-258 are now traced-only.

N2, I-227 on finite sweeps. A computation link that names manuscript lines, and no record or probe, now matches only items that name those manuscript files. I-227 is now traced-only. E2-12 now names the book card table it was checked against (ch01:277–280 at eae01647), so I-361 to I-364 keep reproduced.

N3, chains drifting from their sources. Two new controls:

• merge_matrix.py --check compares matrix.json with the merge of the parts and overlays.
• E4 --check fails when the chains in matrix.json do not carry exactly the corrections in chain-relabels.json.

Both of the reviewer's mutations are now caught: a relabel edited without re-running the merge, and a part file edited alone.

Optional items:

• E1-98's reason for I-088 is corrected.
• E1-71 is recorded as not covering I-149.
• E2-11's failure scope names its reading of L30.
• I-384 and I-385 are now listed by E3-16, E3-17 and E3-18.
• E2_bh02 has a fixed-point control: the length-1 orbits must number N!, which catches a mutant that never applies the permutation.
• b5_check.py now exits 1 when a countercontrol fails.
• The E4 docstring and the rule text now match the code.

Levels (409 rows): 44 reproduced, 127 certificate-checked, 235 traced-only, 3 failed.

Checks: all three --check modes pass, all eight E2 scripts exit 0, the placement and legacy checks pass, and the scan of added lines is clean. Nothing was dispatched. A narrow re-check by the same reviewer is running.

---

Generated by Claude Code

[amaybaum]

Checkpoint 9226b6a5, step 7. The narrow re-check of 8f6ea594 returned ACCEPT WITH CHANGES; its report is retained as review/EVIDENCE-RECHECK-8f6ea594.md.

• The reviewer's findings: N1–N3 are resolved, and so are all five of its optional items. Its independent re-implementation agrees with evidence.json on all 409 rows, and every one of its 14 drift mutations is caught.
• Its one required change, C1, is applied in this commit. For I-227's links 0 and 2, EVIDENCE.md now says that the listed items do not name the link's manuscript file. It previously said they named other records or probes, which was wrong. The rule text now also states that the manuscript match is by file, not by line range.
• Levels are unchanged: 44 reproduced, 127 certificate-checked, 235 traced-only, 3 failed.

Optional, not applied: relabelling I-227's GR and book links as paper-derivation, which would record its reproduced sweeps as the row's artifact level. Its evidence level stays traced-only either way.

Remains for owner authorization (not dispatched):

• a fresh-build CI reproduction of introduction_repro at 17b830bc;
• the BHa and BHb mutants.py replays, and the BHb -O replay;
• the extended expected result for the OD-15 modules, which would be a change on Introduction paper: reconcile sources and integrate scoped theorem recoveries #918. It is time-sensitive while job 121598983127's log exists.

---

Generated by Claude Code

[amaybaum]

PR-AUDIT-1 (#1088): closing without merge

Owner decision (amaybaum, Claude Code session chat, 2026-11-04):

Approved: #942 disposition, steps 1–4 as written. I accept the final independent confirmation and waive the remaining optional fixes. … The reviewed coverage, including the 20 previously untracked findings assigned homes in the drafts, is sufficient for administrative retirement. Closing #942 does not constitute acceptance of its scientific findings.

This PR's audit findings were reconciled against main 27dc3443, and that reconciliation was independently verified twice: ACCEPT WITH CHANGES, then CONFIRMED WITH NITS. Every substantive finding now has a verified disposition: corrected on main, tracked in an open Issue, or superseded with a stated reason. Every remaining item has exactly one Issue home. Proposed transfers are proposals only; none of them is a completed transfer.

• Introduction full-corpus scientific consistency audit (gate for #918) #941, the handoff: the accountable home for every handed-off item until the owner reassigns it. This includes the branch-only findings: FA slice 2 §D D1–D6, Track C I-1–I-12, and the optional O-items.
• Correction planning: scientific overclaims and status corrections (from the 2026-11-01 disposition) #1028, the quoted finding texts and proposed transfers. CON-12 and CON-44 are cross-referenced to their existing home on OI ↔ QM equivalence: proof gate (dependency index; carries #885) #914 and are not duplicated.
• Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029, the SC42 path item and proposed transfers.

No scientific findings of this audit are adopted by closing it. Nothing from this branch lands on main. No theorem grade, claim status or correctness band changes, and no workflow was run.

The branch audit/intro-corpus-20261026 is kept at 16fc745dd0d787d100ca09553bd0342873f26771 as provenance, together with refs/pull/942/head. It is not merged, updated or deleted.

---

Generated by Claude Code