[amaybaum]

Merged: 863637f15fa866da9140682918d9e60bc7531956, normal merge of approved head ed037632368b15612a8553cdb5447d73d4329549 under owner decision c.6687821293. The landed tree exactly matches the independently reviewed tree. Post-merge main CI 42238582109 completed successfully: 25 successful jobs and one skipped. Completion record c.6687977380.

The historical Introduction reproduction record is archived under the existing corpus audit instead of papers/. Its consumers and navigation are updated, and the historical/current reproduction recipes use the correct tool versions. This is repository housekeeping with no theorem, proof-grade or manuscript-claim change.

Merged review target

• Head: ed037632368b15612a8553cdb5447d73d4329549.
• Pre-merge main base: green main f10bb2dd1a53b587b0060b54570b8264dc00d8f1; original drafting snapshot 8925ba46.
• Authority: K1-RDY: paper-only readiness investigation under fixed selection rule #1031 c.6686727803 covers the bounded cleanup corrections; the separate exact-head merge approval is recorded in c.6687821293.
• Integration: ordinary merge of current main into reviewed cleanup 26583468, preserving its history. The cleanup delta against main is unchanged. Fresh required CI 42236506004 completed successfully (25 successful jobs, one skipped); separate integration ACCEPT is c.6687572412. The strict up-to-date rule is recorded in c.6687506996.

Changes

• Move papers/introduction_repro/README.md and results-121598983127.json into verification/audits/manuscript/intro-corpus-audit-20261026/introduction-repro-14/. The old directory is absent from the proposed tree.
• Preserve the JSON byte-for-byte: Git blob 61cfd6ea2df4590cc2ff86f90fc8f50ab71201f7, detected as an unchanged rename.
• Update unit5-evidence/u5_check.py and u5_reextract.py for the current archive path. The checker's pinned f5efa7a0 lookup retains the historical path.
• Repair the root README and introduction-repro-ext/README.md archive links.
• Correct the Unit 5 README's provenance and recipes: current path-maintained script digests are distinguished from original reviewed scripts extracted from b1468584a80746f120ba079924340d6b2430beb2. Dated commands use the original tools, and current-layout commands use the maintained tools. Historical output digests and the reviewed TSV remain unchanged.

Preserved evidence and scope

The 28-module result, original independent Unit 5 review and reviewed TSV are untouched. .github/workflows/evidence-replay.yml, including its historical EXPECTED_14 and EXPECTED_28 commit/path/blob bindings, is untouched; no manual replay is authorized. Dated reviews and closure records keep their original paths as historical provenance. No Lean source, proof/status conclusion, manuscript claim or branch history is rewritten.

Related: completed Introduction corpus audit #941, prior disposition #1138 and #1171. This does not answer the distinct checker-integrity work #1162.

Validation and release gates

• Initial independent review c.6686420619 identified M1/F1; separate correction ACCEPT c.6687377608 closes both at 26583468.
• Original reviewed static tool at historical 424f28b1 and 374b2ef3: both PASS, empty failures, exact retained historical output hashes.
• Path-maintained static check against 26583468: PASS, empty failures, all scanner/mutation controls true, identical pinned/current evidence blobs; c.6687329768.
• Ordinary PR CI 42234887216 succeeded at 26583468 (25 successful jobs, one skipped). Required CI on current integrated head ed037632 is 42236506004, completed/success (25 successful jobs, one skipped).
• No H/F log re-extraction or fresh manual Lean reproduction was performed. Ordinary automatic PR CI is distinct.
• Independent integration ACCEPT c.6687572412 and green exact-head CI were complete before the owner approved and the normal merge landed. Post-merge main CI 42238582109 completed/success at the actual landing (25 successful jobs, one skipped); all required checks passed.

[amaybaum]

Independent exact-head review — ACCEPT WITH CHANGES (material)

Object: #1174 at d76a14a62d6b5e1341f78a74131f056dc2f562db, base 8925ba462da6fa7af30925847c93fb067ccda82d. I did not author this cleanup. The five-path diff is narrow and the evidence move is sound, but the governing Unit 5 recipe and current navigation need correction before merge.

M1 — Repair the governing Unit 5 README's script identities and reproduction recipes.

Location: verification/audits/manuscript/intro-corpus-audit-20261026/unit5-evidence/README.md:32–36, :71–79 and :94–105.

This unchanged README still publishes the original script digests, says the three files besides REVIEW.md are byte-identical to the reviewer's originals, and invokes the scripts from the current checkout against historical targets 424f28b1 and 374b2ef3. Both scripts have changed their current-result P14 path. The relocated path does not exist at either historical target.

The current source hashes at this head are:

file	actual SHA-256	SHA-256 still claimed by the governing README
u5_check.py	012e4322b215104876e7ded45cd799e11ffd4dfce0ea8221a3861877a7af6087	d71bce27256a626f3084c323e5171b2886f7bf9c37fca95f58c6512b4b36efbc
u5_reextract.py	cfed56545d1e0f8a2530dc62a26ff8dd175fb72dc08a12e1ab01615515c69afa	105e7e342e082b5479ad1d94656c81fa83483660d8e0cbd5ad1597bca3ed57f0

I independently ran three bounded static cases from immutable source blobs:

• New u5_check.py against this proposed head: exit 0, PASS, no failures; it finds the unchanged 14-module blob at the new path.
• The same new script against the README's 424f28b1 target: exit 1 before producing JSON, at u5_check.py:161 (json.loads(show(MAIN, P14)) receives None because the new path is absent).
• The original script from 8925ba46 against that same historical target: exit 0, PASS; output SHA-256 is exactly the README's retained d21449aae2c9d596e89cb589601a8ae12c183bbb397c5334ce3c2ca797a06ae4.

The re-extraction recipe has the same lookup problem: new u5_reextract.py:119 reads the relocated P14 at its supplied historical MAIN before opening either log. This was checked from its data flow and the Git tree; I did not download or re-compare the full historical/fresh logs.

Minimal repair: update the governing README to distinguish the original reviewed scripts and dated outputs from the path-maintained scripts. Preserve historical REVIEW.md, TSV, evidence bytes and historical output digests. Make dated recipes explicitly extract/use the original scripts at a named immutable commit, or provide strictly checked backward-compatible path resolution. Give a tested current-layout invocation for the maintained scripts. Update/qualify the current digest table and the byte-identity claim. The old historical output digests must continue to describe their original runs, rather than being silently replaced by current outputs.

This is material because the published recipe currently fails. It is a maintenance/reproducibility correction, with no need for a new Lean build or scientific-status change.

F1 — Update the repository's current navigation link (minor, required integration fix).

README.md:117 still links to papers/introduction_repro/ and says that directory holds the 29-declaration historical evidence and recipe. That path is absent from the proposed tree. Change the link target and its path label to verification/audits/manuscript/intro-corpus-audit-20261026/introduction-repro-14/, preserving the historical-evidence description and declaration count. This is a current reader entry point; the relocation note inside the moved README does not repair the broken root link.

Checks that pass

• The old directory is absent and both moved files are present; Git detects two renames.
• The moved JSON is byte-identical and remains blob 61cfd6ea2df4590cc2ff86f90fc8f50ab71201f7.
• The replay workflow is byte-identical to the base, so its historical commit/blob pins and behavior are unchanged. Its old-path references are intentionally pinned/historical and need no relocation edit.
• The retained 28-module result, Unit 5 REVIEW.md and u5_reports.tsv are byte-identical to the base.
• The edited scripts resolve the old 14-module pin by its historical path and the proposed current copy by its new path as intended; the static check passes for the proposed current tree. Their parsing/comparison logic is otherwise unchanged in this diff.
• git diff --check passes. A read-only clean merge prediction against current main f10bb2dd1a53b587b0060b54570b8264dc00d8f1 preserves the exact reviewed net diff; Structure: remove unresolved attribution placeholder; add AI-disclosure pointer #1165's Structure files are disjoint.
• PR verify 42225364111 is successful at this head. That run does not cure the governing README's failed historical command.

No manuscript, Lean proof, theorem grade, frozen JSON or historical review needs alteration. I made no source edits, branch changes, dispatch or merge. Please publish a corrected immutable head for a bounded delta review and fresh CI, then present that exact head for the owner's separate merge decision.

Prepared by Codex in the current ChatGPT Work session; independent of this PR's author.

[amaybaum]

Narrow correction checkpoint started. Under the owner's follow-up “Ok good, let's proceed as suggested”, recorded at #1031 c.6686727803, the current Codex session takes the two documentary fixes in c.6686420619: root navigation, and the governing Unit 5 tool-version/recipe documentation. The branch is still at d76a14a6, with no intervening writer checkpoint. The correction will preserve scripts/evidence/workflow bytes at this head and add only the required README changes. Its new head will receive separate independent review and ordinary CI; merge remains a separate decision.

Prepared by Codex in the current ChatGPT Work session.

[amaybaum]

Review-fix checkpoint

Pushed 26583468e93161f6266dc303219de593c6b7bdcb, a single-parent, two-README follow-up to d76a14a62d6b5e1341f78a74131f056dc2f562db, under #1031 c.6686727803 and writer record c.6687068755. M1 is addressed by pinning the original reviewed scripts for dated reproduction recipes and distinguishing current script/output identities. F1 is addressed by the root README's new archive link.

The historical static recipes have been executed with the pinned original tool at both documented commits: PASS / failures=[], with exact output hashes d21449aae2c9d596e89cb589601a8ae12c183bbb397c5334ce3c2ca797a06ae4 (424f28b) and 6bbbb1d7496fe56b953ff9ef1bc797ae760533e6374fe492a2abf36b23d2ce2e (374b2ef). The current-layout static case is being confirmed separately. No H/F log replay or fresh Lean reproduction is claimed.

The correction leaves both scripts, the archived JSON blob, the 28-module evidence, REVIEW.md, the reviewed TSV and the historical replay workflow byte-identical to d76a14a. A separate reviewer is checking this authored delta at the immutable 2658346 head; fresh automatic PR CI is pending. Draft and unmerged; separate owner approval remains required.

[amaybaum]

Current-layout recipe check

At exact current head 26583468e93161f6266dc303219de593c6b7bdcb, the path-maintained u5_check.py was extracted from that commit and run with that commit as its source argument: exit 0, structured verdict: PASS, failures: []. All scanner and entry-mutation controls are true. Both the pinned historical and relocated current 14-module paths resolve blob 61cfd6ea2df4590cc2ff86f90fc8f50ab71201f7; the 28-module pin and current blob both remain 97a2377dbfc30987887dffea2b72e423feed079d.

This completes the three bounded static recipe checks reported in c.6687308466. Current output SHA-256 684a3defde3eb450713abd3144727f7d2964d2430edea84e6b3e07165dbb6e85 is provenance for this source identity, not a replacement for either historical digest. No fresh Lean build or H/F replay was performed. Independent delta review and automatic PR CI 42234887216 remain the release gates; no merge is authorized.

[amaybaum]

Transcribed verbatim from the separate independent reviewer /root/review_1169_gate_a. The coordinator authored the two README fixes and did not author this acceptance verdict.

Independent exact-head review — PR #1174 README correction

Verdict: ACCEPT at 26583468e93161f6266dc303219de593c6b7bdcb against its direct parent d76a14a62d6b5e1341f78a74131f056dc2f562db. No material findings remain in this two-README correction.

I did not author these changes. I reviewed the immutable diff, the complete governing Unit 5 README, the original and maintained script sources, their Git objects and hashes, the retained review/TSV references, the replay workflow's historical pins, and #1174 c.6686420619. This review addresses that comment's M1 and F1; it does not repeat the original scientific evidence review.

M1 is closed. The Unit 5 README now distinguishes current path-maintained scripts from the original reviewed tools and dated outputs. I independently hashed the immutable script contents and confirmed every script digest in the revised README:

Tool	Original at b1468584a80746f120ba079924340d6b2430beb2	Maintained at the reviewed head
u5_check.py	d71bce27256a626f3084c323e5171b2886f7bf9c37fca95f58c6512b4b36efbc	012e4322b215104876e7ded45cd799e11ffd4dfce0ea8221a3861877a7af6087
u5_reextract.py	105e7e342e082b5479ad1d94656c81fa83483660d8e0cbd5ad1597bca3ed57f0	cfed56545d1e0f8a2530dc62a26ff8dd175fb72dc08a12e1ab01615515c69afa

The original-tool pin is reachable from source main f10bb2dd1a53b587b0060b54570b8264dc00d8f1. Comparing those originals with the maintained scripts shows only the documented 14-module path maintenance: current P14 moves to the archive, while the historical f5efa7a0 lookup in u5_check.py keeps its original path. Parsing/comparison logic is unchanged.

The extraction recipe at Unit 5 README:72–85 obtains those exact original tools outside the tree and checks their digests. The static, re-extraction and artifact recipes at :87–123 then invoke those extracted versions against their original historical targets. Their argument ordering agrees with the original scripts, and the dated outputs/digests remain unchanged. The historical P14 exists at both 424f28b1 and 374b2ef3; it resolves to the same 61cfd6ea2df4590cc2ff86f90fc8f50ab71201f7 blob as the new archive path and the f5efa7a0 pin.

The separate current-layout instructions at :131–153 correctly use the maintained scripts and name the supplied current HEAD. They do not reuse historical output hashes or silently replace the retained TSV. The historical census count is qualified; the current census checks its current registry. Current re-extraction requires its actual verdict/mismatch result before claiming agreement.

For execution evidence, I read the author's exact-head static-current.json and summary.json and independently verified the output SHA-256 684a3defde3eb450713abd3144727f7d2964d2430edea84e6b3e07165dbb6e85. The JSON names 26583468e93161f6266dc303219de593c6b7bdcb, reports PASS with failures: [], and has all seven scanner controls and eight entry controls true. Its current/historical 14-module blobs are both 61cfd6ea…; its pinned/current 28-module blobs are both 97a2377d…. This is an author-executed static check whose structured output I inspected, not an independent rerun or a new Lean reproduction. The previously reproduced historical static output hashes are preserved; this review did not rerun the H/F re-extraction or artifact layer.

F1 is closed. Root README:117 now links to the existing verification/audits/manuscript/intro-corpus-audit-20261026/introduction-repro-14/ directory. Its README:3–9 confirms the retained description: historical evidence for the 29 baseline declarations at 17b830bc, associated with the Introduction as landed at f5efa7a0. No declaration count or scientific claim changed.

Evidence and scope are preserved. Exactly README.md and unit5-evidence/README.md changed against d76a14a6. The JSON records, scripts, workflow, historical REVIEW.md and TSV are therefore byte-identical to that parent. I also confirmed the retained review and TSV hashes (a92d266b… and 2f4610d5…), and checked the replay workflow's unchanged historical EXPECTED_14/EXPECTED_28 commit, path and blob bindings. The original review, historical results and their qualifications have not been rewritten or promoted.

git diff --check passes. This is a documentation/navigation/reproducibility correction with no scientific scope or status change. I made no repository edits, checkout/ref changes, GitHub posts, scientific computation, Lean build, fresh replay, dispatch or merge. Acceptance of this source correction does not authorize merge.

[amaybaum]

Integration gate — branch update required before approval

The review and CI at 26583468e93161f6266dc303219de593c6b7bdcb pass, but GitHub reports the branch behind main. The active guardrail ruleset 21725642 requires strict up-to-date status checks (Lean kernel check, Mathlib bridge, Numerical probes). Therefore this head is not yet presented for owner merge approval.

Under the existing cleanup authorization #1031 c.6686727803, the designated writer will reconcile current green main f10bb2dd1a53b587b0060b54570b8264dc00d8f1 into the cleanup branch with an ordinary merge commit, preserving reviewed history. The rehearsed merge is clean, tree 5cc5c95a67008fadfb327fb99d36b8ea2ec89fa6, and retains exactly the same seven-path cleanup delta relative to main, including the unchanged JSON rename. The separate reviewer will check that integration at its exact head, and required CI must be green before a separate owner merge decision. Research PR #1173 remains outside this integration.

[amaybaum]

Up-to-date integration checkpoint

Pushed ed037632368b15612a8553cdb5447d73d4329549, parents 26583468e93161f6266dc303219de593c6b7bdcb and current green main f10bb2dd1a53b587b0060b54570b8264dc00d8f1. It is the clean automatic merge tree 5cc5c95a67008fadfb327fb99d36b8ea2ec89fa6. The binary cleanup diff against current main has SHA-256 291f6f63d489b68cc01a50357f92f55c6d86e7874f2257617d68c5d74a4b80b5, identical to the rehearsed seven-path delta. No additional cleanup source edits were made.

GitHub now reports the PR based on f10bb2dd, with the branch-behind condition resolved. Fresh required CI is 42236506004 at this exact head. Separate read-only integration review is assigned to the same independent reviewer, covering the clean merge, the unchanged cleanup delta and preserved evidence/qualifications. Previous correction ACCEPT c.6687377608 and prior-head CI remain provenance; neither substitutes for the current-head gates. Separate merge approval has not been requested yet.

[amaybaum]

Independent integration verdict

Transcribed verbatim from the separate independent reviewer /root/review_1169_gate_a; the coordinator created the integration commit.

Independent integration verdict: ACCEPT at ed037632368b15612a8553cdb5447d73d4329549.

The parents and tree match the stated objects. From merge base 8925ba46, main changes only the three Structure files, disjoint from the cleanup. The integration adds exactly those main changes, byte for byte, establishing the clean automatic merge.

Relative to main f10bb2dd, the identical seven-path cleanup delta remains, with binary-diff SHA-256:

291f6f63d489b68cc01a50357f92f55c6d86e7874f2257617d68c5d74a4b80b5

M1/F1 fixes, historical recipes, script identities, retained JSON/REVIEW/TSV evidence and workflow pins remain intact. No new cleanup claim or scientific scope change was introduced.

git diff --check passes. No source/ref/GitHub changes or scientific reruns were performed. This verdict does not substitute for fresh CI or owner merge approval.

[amaybaum]

Exact-head merge decision packet — all preparatory gates complete

Proposed normal merge: #1174 at ed037632368b15612a8553cdb5447d73d4329549, into current green main f10bb2dd1a53b587b0060b54570b8264dc00d8f1.

• Independent review: original c.6686420619, correction ACCEPT c.6687377608 (M1/F1 closed), exact integrated-head ACCEPT c.6687572412.
• Current-head CI 42236506004: completed/success; 25 successful jobs and one skipped. Required Lean kernel check, Mathlib bridge and Numerical probes are all success. The integrated head contains current main, satisfying the strict up-to-date rule.
• Historical static recipes reproduce both retained output hashes; the current-layout static check passes with all controls. No fresh manual Lean or H/F replay is claimed.
• The reviewed seven-path cleanup delta preserves the JSON bytes, reviewed evidence, historical output identities and replay pins. The merge tree is 5cc5c95a67008fadfb327fb99d36b8ea2ec89fa6; its cleanup diff relative to current main is unchanged from the accepted integration review.
• GitHub reports mergeable/clean. The PR is ready for review, not merged. Research PR OI–QM: interface studies and source assessments #1173 is outside this merge decision.

The owner is being asked for a separate normal merge of this exact head, as reserved by #1031 c.6686727803 and AGENTS.md §A.45. If approved, merge with an expected-head guard, verify the actual landing tree and then require successful post-merge main CI. No force push, squash, branch deletion or scientific claim promotion is proposed.

[amaybaum]

Owner authorization — normal merge of the reviewed cleanup head

Recorded by Codex from the current ChatGPT Work conversation, 2026-11-06 14:57:20 UTC. The owner replied to the exact-head merge proposal c.6687669894 and its confirmation question, verbatim:

Proceed as suggested

The accepted scope is the normal merge of #1174 at ed037632368b15612a8553cdb5447d73d4329549, followed by verification of the actual landing and post-merge main CI. This summary is not a further owner quote. Independent integration ACCEPT c.6687572412 and successful exact-head CI 42236506004 remain the preparatory evidence. Preflight confirms the same head, current main f10bb2dd1a53b587b0060b54570b8264dc00d8f1, and GitHub mergeable/clean.

Research PR #1173 and later research gates remain outside this merge decision.

[amaybaum]

Landing verified — post-merge CI pending

Under recorded owner approval c.6687821293, the normal merge of exact reviewed head ed037632368b15612a8553cdb5447d73d4329549 landed as 863637f15fa866da9140682918d9e60bc7531956.

The host commit and PR records confirm parents f10bb2dd1a53b587b0060b54570b8264dc00d8f1 and ed037632368b15612a8553cdb5447d73d4329549, and tree 5cc5c95a67008fadfb327fb99d36b8ea2ec89fa6, exactly the independently accepted integration tree. The merge has exactly the seven reviewed file changes; the historical JSON is an unchanged rename with blob 61cfd6ea2df4590cc2ff86f90fc8f50ab71201f7. Evidence bytes, historical tool/output identities, review/TSV records and workflow pins are preserved as reviewed. Main now points to this merge.

Post-merge verify run 42238582109 is a push run at this exact landing SHA and is queued/running. Completion will be recorded only after its structured run/job conclusions succeed. Research #1169 / #1173 and later research gates are outside this merge; their authorization/status is unchanged.

[amaybaum]

Completion verified — merged and main CI green

#1174 is merged normally as 863637f15fa866da9140682918d9e60bc7531956, from the exact owner-approved head ed037632368b15612a8553cdb5447d73d4329549 (owner decision c.6687821293). The PR is closed/merged, and current main points to this landing.

The landing verification in c.6687853522 confirms the two expected parents, the exact accepted tree 5cc5c95a67008fadfb327fb99d36b8ea2ec89fa6 and the reviewed seven-path cleanup delta. The relocated historical JSON retains blob 61cfd6ea2df4590cc2ff86f90fc8f50ab71201f7; the historical evidence, review/TSV identities and replay pins are preserved as independently reviewed.

Post-merge main CI: verify run 42238582109, event push, exact head 863637f15fa866da9140682918d9e60bc7531956: completed/success. The structured host job records show 25 successful jobs and one skipped, with required Lean kernel check, Mathlib bridge and Numerical probes all completed/success.

The authorized cleanup and its merge verification are complete. No scientific claim or proof grade is promoted. Research #1169 / guiding draft #1173 remains at its reviewed conditional paper checkpoint; no later research gate is activated by this completion.

[amaybaum]

Owner-authorized README follow-up

The owner, in the current ChatGPT Work conversation on 2026-11-06, approved the narrow README simplification, verbatim:

Ok please proceed as suggested

The accepted suggestion is to retain “Its proofs and their verification are in the formal papers it cites.” and remove only the following historical archive sentence from the root README's Introduction entry. The detailed history and retained evidence stay in the archive unchanged.

Codex is the designated writer for this one-sentence README edit, from current green main 863637f15fa866da9140682918d9e60bc7531956. The seven currently open PRs were checked; none changes the root README. The follow-up will have its own scoped draft PR and ordinary CI. This is editorial drafting; integration remains separately gated by AGENTS.md §A.45. #1116's credit question and research authorizations are unaffected.