[amaybaum]

Draft. Merge is not authorized; the owner decides separately.

This PR updates the README and other documentation for the Introduction paper, which landed in #1124 (f5efa7a0), at the owner's request. It also redraws the README's correspondence diagram, which the owner asked for.

Changes (head 6f4073b8; net diff against main 5e35eb88)

• README.md
  • "Start here": new first row, "A short introduction to the framework's finite-observer results → papers/Introduction.md".
  • "Other materials in papers/": new entry describing the paper within its own scope. It points to Appendix A, which lists the Lean declarations the paper cites and their verification status. It also points to papers/introduction_repro/, which holds the axiom reports for the paper's baseline declarations and the recipe that reproduces them.
  • "The foundational correspondence": the text block is now a left-to-right Mermaid flowchart, S ⇄ D ⇄ Q_fb, with thick two-way arrows and no labels. The node labels match the old text block word for word. The sentence below the diagram still states the equivalence.
• build.sh: the usage comment "build everything (12 papers + book)" now says 13, matching the 13 papers/*.md on main. Behaviour is unchanged.
• .zenodo.json: the description now lists "the introductory paper Introduction (an introductory entry point to the finite-observer results)" among the papers. The file is still valid JSON, and description is its only changed key.

Review

• Short independent review: ACCEPT WITH CHANGES (c.6656883592). It confirmed:
  • the scope is only these three files;
  • the README text claims nothing beyond what the paper itself says;
  • the diagram is consistent with the surrounding text;
  • book/README.md:110 ("twelve technical papers") is correct as it stands;
  • SC-42 passes.
• Requested wording changes, applied in 6f4073b8:
  • "self-contained" is dropped, because the paper refers readers to Main and the companions for the core proofs;
  • the axiom reports are scoped to the baseline declarations.
• Next: a delta check of 6f4073b8 and CI at this head.

Deliberately unchanged

• book/README.md:110: the Introduction is not a source for the book.
• AGENTS.md: it lists papers with "…".
• Manuscripts and records: no manuscript, book, ledger, census or verification file changes, so no rebuild is needed. The formatting fix to the Introduction's header is the separate draft Introduction: use the papers' standard header instead of the pandoc % title block (formatting only) #1128.

🤖 Generated with Claude Code

https://claude.ai/code/session_011zDyUSyEszk3JJx83uXKKq

[amaybaum]

Independent review at head 1fa82546: ACCEPT WITH CHANGES. Two small wording fixes and a stale PR description. Nothing blocks the merge on substance.

Checked and OK

• Scope. The net diff against main 5e35eb88 touches only README.md (+7/−5), build.sh (one usage comment line) and .zenodo.json. .zenodo.json parses, and description is the only key that changed.
• build.sh. main has 13 papers/*.md files, and the no-argument for md in papers/*.md loop builds all of them, so "13 papers + book" is correct.
• Introduction descriptions. The "Start here" row and the topic list in the "Other materials" entry match the paper's abstract and §§2.2, 2.4, 2.5 and 5. "Appendix A … with their verification status" matches the appendix title. Nothing is called proved or machine-checked beyond what the paper says. papers/introduction_repro/ exists on main.
• Mermaid diagram. flowchart LR with three nodes (S, D, Q_fb) and two unlabelled <==> links; the syntax looks valid. I checked it by inspection only and did not render it. The three descriptions match the old text block word for word. With the "exact" labels gone, the diagram shows a two-way link, which agrees with the sentence below it ("The representation equivalence is universal at this finite-record level") and with the S ⟺ D ⟺ Q_fb entry in the Core papers table.
• book/README.md:110. "twelve technical papers" is correct: no book chapter draws on the Introduction. No other README-like file lists every paper. book/bibliography.md:9 paraphrases the old Zenodo list, but it is a book manuscript and already leaves out Computation, so it needs no change here.
• Hygiene. The added lines contain no local paths and no scratch-area wording. check_sc42_integration.py in a detached worktree of the head: verdict: PASS, 689 checks ok, 0 failed.

Changes requested (wording only)

1. "self-contained". The README entry says "short, self-contained introduction" and .zenodo.json says "a self-contained entry point". The paper never calls itself self-contained, and §1.2 sends the reader to [Main] for the core arguments: "The core finite-law and memory arguments are in [Main]; proofs and qualifications also occur in the companion papers…". Suggest "standalone" or "introductory", or dropping the adjective.
2. Scope of the axiom reports. "the axiom reports and the recipe that reproduces them are in papers/introduction_repro/" reads as if it covered every declaration in Appendix A. The repro covers only the 28 baseline declarations at 17b830bc. The paper's Code section separates out the four additional modules (RecordFibreIdentification, RootedRecurrenceBridge, TrajectoryMemory, FullFutureMemory): they are built on main, and their proofs have not been independently reviewed. Suggest "…the axiom reports for its baseline declarations, and the recipe that reproduces them, are in …".
3. PR description is stale. It still names head f99e3d8a and says each link is labelled "exact". Please update it to the current head and the unlabelled <==> links.

CI at 1fa82546 (run 42019215000): still running when I checked. Lean kernel check and 15 probe jobs have passed, one matrix job was skipped, and none has failed. Mathlib bridge, core A/B and seven other probe jobs were still running.

---

Generated by Claude Code

[amaybaum]

Delta review, 1fa82546 → 6f4073b8: ACCEPT.

• Only the two requested wording fixes. The commit touches two files, one line each:
  • .zenodo.json: "(a self-contained" → "(an introductory".
  • README.md, Introduction entry: "short, self-contained" → "short"; "the axiom reports for its baseline declarations, and the recipe that reproduces them, are in …".
  • The only "self-contained" left in README.md is the Juno row on Start here, which was already on main. The added lines contain no local paths or scratch-area wording.
• .zenodo.json parses. Against main 5e35eb88, the only key that differs is description. The net diff against main is still only README.md, build.sh and .zenodo.json.
• SC-42 at 6f4073b8, run in a detached worktree: verdict: PASS, with 0 failed checks.
• PR CI at 6f4073b8: verify run 42019670604 finished with conclusion success.

This resolves the three findings from my earlier comment (#issuecomment-6656883592), provided the PR description is updated as planned.

---

Generated by Claude Code

[amaybaum]

Merge record.

• Merge: c88293e4f0a20af2c1a290f77ba1d9c3bda600ab, a normal merge commit with expectedHeadSha 6f4073b8. The owner's approval is quoted on Introduction paper: reconcile sources and integrate scoped theorem recoveries #918 (c.6657303442).
  • Parents: 5e35eb88 (main) and 6f4073b8 (the reviewed head).
  • The merge tree equals 6f4073b8's tree.
  • The net change touches only README.md, build.sh and .zenodo.json. Both approved wording corrections are intact.
• Reviews: short review c.6656883592, then a delta check, ACCEPT (c.6657092310). PR CI run 42019670604 at 6f4073b8 was green.
• main CI: push run 42022612501 on c88293e4 concluded success. That includes the Mathlib bridge release gate, whose legacy-records step confirms the 303 legacy records are intact.

---

Generated by Claude Code