[amaybaum]

Draft. Merge is not authorized. The owner decides on the exact reviewed SHA separately.

This is the narrow landing of the Introduction approved on #918:

• D1–D12, c.6650823924;
• V-O3, c.6651201185;
• option (b), c.6655644630.

It carries the five reviewed files and the six INTRODUCTION:* ledger rows. It excludes the other 281 files on #918's branch, and #918's branch is kept. The [CE]/[CR] evidence commits are already reachable from main through #1117 (53a3eb3d).

Status at head ba92a6cc8313625bc2bbdd2e4becf20507d27358

• Independent review: ACCEPT (c.6655788106). All ten checks pass at this exact head. The reviewer's own countercontrols also pass:
  • another all-caps word is still flagged;
  • REST alone is not flagged;
  • removing REST brings back the README:105 hit.
• PR CI: verify.yml run 42010587847 (pull_request, head_sha ba92a6cc) concluded success: 25 jobs passed and 1 was skipped (the dispatch-only A42 matrix).
  • The jobs that passed include the Mathlib bridge release gate, the Lean kernel check and the core-B SC-42 step.
  • The run used a synthetic merge, but the merge tree equals the head tree.
• Mergeability: clean, with main at 4b4b437c.

Commits

Commit	Content
40fc5954	C1: verbatim copies from #918 head 44236326 (2a2b1481, 29016952, aa6b45ef, 18e14459, 61cfd6ea) plus the six ledger rows
719af26b	C2: the approved text corrections (D3, D6, D8, D9, V-O3, SC-42), independently reviewed (record on #918 c.6655356740)
7eef801d	SC-42 checker: REST added to CAPS_OK (owner option (b))
0ea4ae4c	Repro README:105 restored to the reviewed original "through the REST API (…)"
51c34355	sh ./build.sh Introduction: 25 pages, 0 dropped glyphs
ba2c81f7	Ledger L120 row regenerated (D6)
e12863d5	Merge of main 4b4b437c (no conflicts; the LEDGER.json result is the union)
ba92a6cc	SC-42 committed result and controls regenerated

40fc5954 and 719af26b are preserved unrewritten.

Net change against main 4b4b437c (9 files)

• papers/Introduction.{md,tex,pdf}
• papers/introduction_repro/README.md
• papers/introduction_repro/results-121598983127.json
• the six INTRODUCTION:* rows in verification/coverage/LEDGER.json (+84 lines)
• the three SC-42 files described below

The Introduction has 483 lines against 485 at 44236326. The net −2 comes from deleting the [CT06] entry (−2) and the unused [HLW06] entry (−2), and adding the D3 split paragraph (+2). The unused [PSW06] entry's place is taken by [PW25].

The SC-42 change (owner option (b))

• The checker. check_sc42_integration.py adds 'REST' to CAPS_OK, with a comment: REST names GitHub's REST API (Representational State Transfer), an abbreviation, not emphasis. The patterns and the nine mutation controls are unchanged, and paper_caps (EMPHASIS) still fails its mutant. README:105 is the only REST in papers/.
• The two committed outputs. sc42-integration-result.json and sc42-integration-controls.json each differ from main only in checker_sha256 (c767d094… → 447e0531…). The normal and -O outputs are byte-identical.

Ledger L120 (D6)

Changing [CT06] to [PW25] at Introduction.md:120 changes the text-derived identity of the unnamed Corollary:

Field	Before	After
id	INTRODUCTION:C-unnamed-b596be8a	INTRODUCTION:C-unnamed-99fe05c0
fingerprint	b596be8af06bd797	99fe05c0d24d20c3

These were recomputed by tools/proof_census.py --json, and the rest of the row is unchanged. The old id was never on main.

Checks

• Pass: coverage (140 statements), duplicate, staleness, voice, claims, lean_manuscript_census, artifact_placement_check, dependency_label and baseline_label.
• SC-42: PASS, equal to the committed files.
• On full history (the reviewer's clone): legacy_records_check reports 303 records intact, and citation_roles_check passes.

Known minor item (not changed here)

Repro README:63 says "The 28 declarations of Appendix A", but Appendix A also cites c3_necessity_via_hidden. That declaration's axiom report is in the results JSON. The text is inherited verbatim from the reviewed blob 18e14459 and changes no claim. It is left for a later one-row correction.

Limits and routing

• Six sites (L116, L126, L128, L138, L158, L174) say "machine-checked" for the four Lean-only families. That is consistent with the L43 convention. They are routed to Independent review and census disposition of the four kernel-only Lean families the Introduction cites #1118 (D10) and not edited here.
• This landing changes no scientific status.
• Issue Introduction paper: reconcile sources and integrate scoped theorem recoveries #918 stays open; closing it is a separate owner decision.
• A merge, if authorized, uses a normal merge commit with expectedHeadSha.

Links: #918, #941, #1117, #1118, #970, #1028, #1015.

🤖 Generated with Claude Code

https://claude.ai/code/session_011zDyUSyEszk3JJx83uXKKq

[amaybaum]

Independent review of PR #1124 at exactly ba92a6cc8313625bc2bbdd2e4becf20507d27358 (base main 4b4b437cfff9dcf32c882251d1a4c3445ca9e8be)

• Who and how. This is a read-only, model-authored review by an agent that did not write this landing. It is not an authenticated human review.
• Clone. A fresh full clone (--no-local, not shallow, no alternates) with the PR branch fetched. git ls-remote confirmed the branch at ba92a6cc and main at 4b4b437c.
• What I did not do. No commits, pushes, dispatches or Lean builds. The only build was sh ./build.sh Introduction. All temporary edits for countercontrols were made in the clone and reverted.

Verdict: ACCEPT

Every item checks out at the exact head. The two non-blocking notes at the end need no change before the owner's merge decision.

1. Scope: CONFIRMED

git diff --stat 4b4b437c ba92a6cc is exactly 9 files (+5865/−3):

• papers/Introduction.{md,tex,pdf};
• papers/introduction_repro/README.md;
• papers/introduction_repro/results-121598983127.json;
• verification/coverage/LEDGER.json: +84/−0, only the six INTRODUCTION:* rows. Every other entry and every top-level key equal main's;
• check_sc42_integration.py (+2/−1), sc42-integration-result.json (±1) and sc42-integration-controls.json (±1).

Further structure:

• Merge tree. git merge-tree origin/main ba92a6cc gives tree a17cdf4a, the head's own tree. The PR CI's synthetic merge therefore tested exactly this content.
• Commit scope. Each post-C2 commit touches only what the PR body says. e12863d5 resolves LEDGER.json as the union.

2. C1 integrity: CONFIRMED

• Blobs. At 40fc5954 the five files are 2a2b1481, 29016952, aa6b45ef, 18e14459 and 61cfd6ea, identical to Introduction paper: reconcile sources and integrate scoped theorem recoveries #918 head 44236326.
• Ledger rows. The six INTRODUCTION:* rows equal Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's as parsed JSON. The added-line hunk (53a3eb3d..40fc5954) is byte-identical to Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's (f6989a27..44236326), 84 lines.
• History. 40fc5954 and 719af26b are ancestors of the head, unrewritten: the parent chain runs 40fc5954 → 719af26b → 7eef801d → 0ea4ae4c → 51c34355 → ba2c81f7 → e12863d5 (+ main) → ba92a6cc.

3. Manuscript: CONFIRMED

papers/Introduction.md is byte-unchanged since 719af26b. In the repro README, only line 105 changed after 719af26b.

README:105 equals line 105 of blob 18e14459 byte for byte ("…through the REST API (actions/jobs/121598983127/logs) on"). Against 18e14459 the README now differs only at L110, the C2 SC-42 fix that put backticks around the three step identifiers.

C2 (40fc5954..719af26b), word-diffed against the rulings:

• D3. The four kernel-only families are moved out of "Established mathematical results" into a separate paragraph headed "Checked in Lean, not independently reviewed:" (L324). The baseline list stays in L322. Appendix A is retitled "Lean declarations and verification status", and no old-title reference remains anywhere in papers/ or book/.
• D6. [CT06] → [PW25] at L118, L120, L124, L138 and L353. The reference reads "Y. Polyanskiy and Y. Wu, Information Theory: From Coding to Learning, 1st ed. (Cambridge University Press, 2025)".
  • Locators. I checked them first-hand against the authors' CUP prepublication export (itbook-export, CUP/HE2 design, 16 Aug 2024, which says it "will be published by Cambridge University Press"). Thm 3.7(a) is "I(X;Z|Y) ≥ 0, with equality iff X → Y → Z", the vanishing criterion used at L118, L120, L138 and L353. Thm 7.10 is Pinsker's inequality, D(P‖Q) ≥ (2 log e) TV², which gives the bits-form floor at L124.
  • Print edition. Retailer listings confirm CUP 2025 (ISBN 9781108832908). I did not inspect the printed book's numbering.
  • Text. The manuscript cites [PW25] without theorem locators, as it did [CT06]. No [CT06] remains.
• D8. [BHa] and [BHb] carry the approved reader-facing descriptions, ending "not a derived physical model of black-hole evaporation". The cited paths verification/programmes/black-hole-information/bh0{1_access,2_scramble}_v1/ exist on main.
• D9. [HLW06] and [PSW06] are deleted, and neither is cited anywhere.
• B3. The BH-01 language is narrowed through D8, R-21 and V-O3's L302/L304 changes. The V-O3 audit verified L41 as accurate.
• R-21 and V-O3, exactly as approved in c.6651201185:
  • L134: "is proved on paper in the coupling-step model";
  • L302: "…at small size; the maps range over all bijections, or all maps, of the register space, and none is derived from the substratum's dynamics.";
  • L304: "60 non-injective maps of ${0,1}^2$, with a one-bit message and the other register uniformly random, recover…".
• SC-42 fixes. L99 "no longer shows" → "does not show", with the meaning unchanged. README L110 adds the identifier backticks.
• Nothing else changed in the text.
• Line count. 483 lines.

4. SC-42 checker: CONFIRMED

The checker diff is exactly 'REST' appended to CAPS_OK, plus one comment line: "REST is the name of GitHub's REST API (Representational State Transfer), an abbreviation, not emphasis." The patterns, scan logic and nine MUTATIONS are untouched.

Runs from the clone root:

• python3 -I -B … --verbose: exit 0, PASS, 689 checks, 0 failed predicates, "added-text scan: 0 hit(s)" over 53,069 chunks. The -O run is byte-identical.
• --self-test, normal and -O: byte-identical, verdict PASS, all 9 controls passed. paper_caps still fails its mutant ("added-text scan: 1 hit(s)").
• Committed files. Both equal the fresh outputs byte for byte. Against main each differs only in checker_sha256 (c767d094… → 447e0531…).

My countercontrols (in the clone only, then reverted, after which git status was clean):

• (a) Appending "this is IMPORTANT for the record." to the repro README: exit 1, hit ('papers/introduction_repro/README.md', 'caps', 'IMPORTANT').
• (b) Appending "…through the REST interface.": exit 0, 0 hits.
• (c) Removing 'REST' from CAPS_OK at the head: exit 1, hit ('…/README.md', 'caps', 'REST'). So the allowance is necessary for README:105, and it admits nothing else: README:105 is the only REST in papers/.

5. Ledger L120: CONFIRMED

• At the head. tools/proof_census.py --json gives INTRODUCTION:C-unnamed-99fe05c0 with fingerprint 99fe05c0d24d20c3 at line 120.
• At 40fc5954. The same tool gives …-b596be8a / b596be8af06bd797.
• The row. Comparing the row between 40fc5954 and the head, only id and fingerprint differ. All six rows match the census's lines and fingerprints.
• coverage_check: OK, 140 canonical statements.

6. Build: CONFIRMED

• Stamp. The .tex stamp 2914ade9… equals the sha256 of the .md.

• Committed PDF. pdfinfo: 25 pages.

• Rebuild. sh ./build.sh Introduction (pandoc 3.1.3, xelatex) gives:

  • a .tex byte-identical to the committed file;
  • identical pdftotext -layout output;
  • 25 pages and 0 "Missing character" warnings.

  The PDF bytes differ only in build metadata, as expected.

7. Full-history checks: all OK

• legacy_records_check ba92a6cc: "303 record(s) in 75 closed namespace(s), all intact".
• citation_roles_check ba92a6cc: self-test OK, all hold.
• OK: duplicate, staleness (14 matched), voice (41 files), claims, lean_manuscript_census, artifact_placement_check, dependency_label_check and baseline_label_check.
• The SC-42 files are not in the legacy manifest or in any receipt or seal.

8. Register and §A.42 item 8

§A.32/§A.33. Every line of the Introduction and the repro README is newly added on main. None hits the register or revision-history families.

The 4+-letter capitals are all acronyms or identifiers: CHSH, CADE/SIGPLAN, KTOKEN/KTRANS/…, REST, and a quoted AUTHORIZATION: basic ***. The exception is "DRAFT PRE-PRINT" in the L10 status line, which is the header that Main, GR, SM and the other papers use.

No local paths or secrets.

Identifiers in the landed files, each traced:

• Introduction. 17b830bc, f5c281ae, 3d54ae74, 4f962b6, 96a3020b and a958bc54 are commits reachable from main. So are bdcbd32 [CE] and 2624d49 [CR], through #918 B1: retain the [CE]/[CR] evidence commits by ancestry only (history-only merge, no file changes) #1117's 53a3eb3d. These are support on main.
• Repro README and JSON:
  • 17b830bc, 687e885b, 48b18ac5 and 5c4e5087 are on main.
  • Trees 277d2822 and 8624ba39 equal verification/lean and verification/lean-mathlib at both 687e885b and 17b830bc.
  • Blob e6f69713 equals 48b18ac5:verification/audits/evidence-retention/extract_result.py.
  • The remaining 40-hex ids are commits of external repositories (Lean, Mathlib and its dependencies), labelled as such. They are environment provenance.
  • Run 40330683786, job 121598983127 and Book and GR: black-hole statements at the strength of their support #936 are provenance. The result to expect is the committed JSON, with its recipe.
• LEDGER and checker. No ids.
• PR body. #918 B1: retain the [CE]/[CR] evidence commits by ancestry only (history-only merge, no file changes) #1117 is support on main (53a3eb3d). Independent review and census disposition of the four kernel-only Lean families the Introduction cites #1118 exists as the D10 accountable Issue. The other links are provenance.

9. PR CI: green

Run 42010587847 (verify.yml, event pull_request, head_sha ba92a6cc, attempt 1) completed with conclusion success. From the structured job and step records:

• Overall. 26 jobs: 25 success and 1 skipped (A42 exclusion (matrix), which runs only on dispatch).
• Mathlib bridge: success.
  • Build, Release gate and the KTOKEN-MAXCONE-1, PRESERVE-INDUCT-1 and KTRANS-SEP-2 steps succeeded.
  • The "marker complete reports with an axiom outside the three" step was skipped, meaning its condition was false.
• Lean kernel check: success.
• core B: success, including "SC-42 integration source scope and must-fail controls". Under set -euo pipefail, that step cmps the normal and -O outputs and the self-tests against the committed files.
• Aggregate. The "Numerical probes" job succeeded at "Require every probe shard".
• Equivalence to the head. This is a pull-request (synthetic-merge) run, not an exact-head dispatch. Because the merge tree equals the head tree, it tested this content.

10. Mergeability and PR body

• Mergeability. mergeable_state: clean. The PR is still a draft, and main is unchanged at 4b4b437c.
• PR body. Accurate, except for the two notes below.

Non-blocking notes (no change needed for this landing)

• N1. PR body.
  • "legacy_records_check and citation_roles_check report UNDECIDABLE in this shallow clone" is now superseded: on full history both hold (303 intact; citations hold).
  • The 485 → 483 explanation is imprecise. The net −2 is CT06 (−2) + HLW06 (−2) + the D3 split paragraph (+2), with PSW06's entry replaced by PW25. The count itself is right.
• N2. Repro README:63. It says "The 28 declarations of Appendix A", and its table lists 28. Appendix A also cites the baseline declaration c3_necessity_via_hidden (C3Necessity:88, L356), whose report is present in results-121598983127.json, as expected.modules["OIBridge/C3Necessity.lean"].reports[2]. The evidence is complete; only the README's table and count omit it.
  • This was inherited verbatim from the reviewed blob 18e14459, and the landing-gate assessment (c.6649656506) flagged it as minor.
  • It changes no claim. It can be fixed later, or now by a one-row correction if the owner wants it.

Not checked: the printed book's theorem numbering (only the CUP prepublication export); Lean builds; PDF pixels.

Landing gate: all ten requested checks pass at ba92a6cc. This review does not authorize a merge; that remains the owner's separate decision.

---

Generated by Claude Code

[amaybaum]

Merge record.

• Merge. #918 landing: the Introduction (five files + six ledger rows), with the SC-42 REST allowance #1124 was merged as f5efa7a0813218b580272f7fd80a6b0c87eb6657, using a normal merge commit with expectedHeadSha ba92a6cc. This follows the owner approval quoted on Introduction paper: reconcile sources and integrate scoped theorem recoveries #918 (c.6656173399).
  • Parents: 4b4b437c (main) and ba92a6cc (the reviewed head).
  • The merge tree equals the reviewed head's tree (a17cdf4a). The net change against 4b4b437c is the 9 reviewed files (+5865/−3), with no unreviewed content.
• main CI. Push run 42014610097 on f5efa7a0 concluded success. That includes the Mathlib bridge Build and Release gate steps, the Lean kernel check, and core B's SC-42 step.
• Legacy records. The release gate's legacy-records step passed within that run. The independent review found 303 records intact on full history for the same tree.

The Introduction (#918) is now on main. Issue #918 stays open; closing it is a separate owner decision.

---

Generated by Claude Code