[amaybaum]

Draft. Merge not authorized. This PR is presented for a separate merge decision after independent review and exact-head CI.

Authority

Owner decision on #941, comment 6658967061 (amaybaum, 2026-11-05), approving Option (b) of the proposal in comment 6658728711:

Approve Option (b): prepare a separate draft PR preserving the exact 97a2377d evidence blob and a provenance/status README in a canonical verification directory. Requirements: Preserve the blob byte-identically. Explicitly label the 28-module result as not independently verified on main. Do not treat evidence retention as scientific acceptance. Keep the existing staging branch and workflow pin unchanged. Do not merge the 38 historical #918 commits merely to retain this evidence. Obtain independent review and exact-head CI. Present the resulting PR and SHA for a separate merge decision. The workflow's dependency on the staged commit remains an independent unresolved issue.

What is retained, and where

One commit, 2714278a7dd9057a73610658478661065152ca97, single parent d9f0a845 (main), adding two files under verification/audits/manuscript/intro-corpus-audit-20261026/introduction-repro-ext/:

• results-121598983127-28.json: byte-identical to blob 97a2377dbfc30987887dffea2b72e423feed079d, i.e. papers/introduction_repro/results-121598983127.json at e73f7be3 on staging/introduction-repro-ext-20261027. git hash-object on the file and git rev-parse HEAD:<path> both return 97a2377d….
• README.md: what the file is, its recipe, provenance with each off-main reference classified under §A.42 item 8, its relation to evidence-replay.yml, and the remediation route.

Placement (§A.36). intro-corpus-audit-20261026/ is an existing audit directory on main (its tracks/ hold SC-17 to SC-45), and evidence-replay.yml's header names it as the audit that this evidence serves. The new subdirectory is the one the proposal named. The -28 suffix keeps the file distinct from the 14-module file of the same job in papers/introduction_repro/.

Why (§A.46 item 2). A record on main, evidence-replay.yml (EXPECTED_28, and the governed-module step), relies on this blob, which until now existed only on a staging branch.

Content check. Every field except expected.modules matches main's 14-module file (blob 61cfd6ea). The 14 shared module entries match entry for entry. The file adds 14 modules, for 534 reports in all.

Status

The 28-module result is not independently verified on main. It supports no manuscript claim, it is not an accepted result, and retaining it promotes and strengthens nothing (§A.42 item 6; §A.46 items 1, 3, 4 and 7). The review and replay reports on #942 (c.6434184021, c.6435469998) are author-posted, and the README cites them as provenance only. The accountable Issue is #941.

Unchanged

• staging/introduction-repro-ext-20261027 is still at 0a8f4930, untouched.
• .github/workflows/evidence-replay.yml is not touched, and the EXPECTED_28 pin is still e73f7be3. The workflow still resolves the blob through that staged commit; that dependency is a separate unresolved issue on Introduction full-corpus scientific consistency audit (gate for #918) #941.
• None of Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's history is merged. e73f7be3, 24e70304 and 4a260ca9 are not ancestors of this head.
• No papers/ file is changed.

Checks (local, at 2714278a)

• artifact_placement_check: OK, with its self-test. Neither the migration manifest nor the legacy records were edited.
• duplicate_check: OK.
• legacy_records_check 2714278a…: self-test OK, verdict UNDECIDABLE (shallow-repository) in this shallow checkout. It is left to CI's full-history run.
• SC-42 integration check (bell-operational-reconciliation-20261029/check_sc42_integration.py): the normal, -O and committed sc42-integration-result.json outputs are byte-identical. The added-text scan finds 0 hits. The --self-test output equals the committed sc42-integration-controls.json.
• A scan of both added files for tokens, keys, signed URLs, e-mail or IP addresses, and local paths found nothing.
• Ancestry was checked in a commits-only clone of main: 17b830bc and 48b18ac5 (the recipe's commit and tools) are reachable from main.
• Push triggers: only bg2-orientation-design.yml and bridge-compatibility-research.yml have branch-agnostic push path filters, and neither matches this path. verify.yml and hidden-sector-replay.yml push only on main, so the branch push started no workflow. This PR runs the ordinary pull_request CI. That is not an exact-head attestation, and nothing was dispatched.

Outstanding before a merge decision: an independent review, and exact-head CI at 2714278a (needs separate authorization if it requires a dispatch).

---

Generated by Claude Code

[amaybaum]

Independent review of 2714278a — verdict: ACCEPT

I did not write this change. I checked it read-only in a fresh, full-history clone (git clone --no-local, not shallow, no alternates), which I deleted afterwards. The four optional nits below do not block a merge decision.

1. Scope

• 2714278a has a single parent, d9f0a845, which is still main's tip.
• git diff --name-status d9f0a845 2714278a shows exactly two additions, both under verification/audits/manuscript/intro-corpus-audit-20261026/introduction-repro-ext/: README.md (66 lines) and results-121598983127-28.json.
• No changes to .github/, papers/ or anything else.
• staging/introduction-repro-ext-20261027 is still at 0a8f4930.
• 4a260ca9, 24e70304, e73f7be3 and 0a8f4930 are not ancestors of main or of this head, so none of Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's history is merged.
• evidence-replay.yml is unchanged: EXPECTED_28: e73f7be3… and EXPECTED_28_BLOB: 97a2377d….

2. The blob

These all return 97a2377dbfc30987887dffea2b72e423feed079d:

• git rev-parse HEAD:<path>
• git hash-object <path>
• git rev-parse e73f7be3:papers/introduction_repro/results-121598983127.json
• the same path at 24e70304 and at the staging head

3. Placement (§A.36)

• intro-corpus-audit-20261026/ already exists on main, with tracks/ in it. The new subdirectory sits inside that audit directory, not at the verification/ root.
• artifact_placement_check: OK, self-test passed.

4. README accuracy

Status wording. It says the result is not independently verified on main, supports no claim, is not accepted and promotes nothing, and it names #941 as the accountable Issue. This matches #941 c.6658967061 and the proposal c.6658728711.

JSON claims, checked independently:

• oi-evidence-result, version 1, kind bridge.
• Every field except expected.modules is equal to main's 14-module file (blob 61cfd6ea, which is also 24e70304^'s blob).
• The 14 shared entries are identical.
• The 14 added module names are exactly the ones listed.
• There are 534 reports and 534 prints.

The README does not claim that all reports use the three standard axioms. That is correct: PhysicalCharacterization.levelOne_eq reports [propext] only.

Provenance claims:

• 24e70304 (parent 4a260ca9) changes the JSON from 61cfd6ea to 97a2377d, plus the staged README.
• e73f7be3 changes only papers/introduction_repro/README.md. The JSON is unchanged.
• Run 40330683786 is verify.yml, a push at 17b830bc. Its job 121598983127 is "Mathlib bridge" (success). The JSON's run block agrees.
• In the recipe, 48b18ac5:…/extract_result.py is blob e6f69713, as the JSON's source states.
• Audit: the Introduction against the full core OI corpus (gate for #918) #942 c.6434184021 does report an independent review of the staged result with ACCEPT WITH CHANGES, and README fixes applied at e73f7be3 with the JSON unchanged.
• Audit: the Introduction against the full core OI corpus (gate for #918) #942 c.6435469998 does report fresh-build run 40457712855 comparing against expected-28 = e73f7be3 / 97a2377d.

§A.42 item 8.

• 17b830bc and 48b18ac5 are reachable from main, so they are support on main for the recipe.
• 24e70304 and e73f7be3 are not reachable from main. Each is correctly classified as provenance: the only content used from them is the blob, which this commit lands.
• The two Audit: the Introduction against the full core OI corpus (gate for #918) #942 reports, the job and the run are correctly classified as provenance only.
• I also traced the references the table does not list:
  • Introduction full-corpus scientific consistency audit (gate for #918) #941 c.6658967061 and c.6658728711: authority for retaining the file. No result claim uses them.
  • The staging branch name: provenance.
  • Introduction full-corpus scientific consistency audit (gate for #918) #941 as the accountable home: planning.
• None of these is support off main, so there is no gap.

Overstatement. None. The README says outright that REPRODUCTION HOLDS "has not been established from main", and that the pin is not made durable.

Secrets and local paths. A scan of both files for tokens, keys, signed URLs, e-mail or IP addresses, and /home or /tmp paths found nothing.

5. Full-history checks at 2714278a

• legacy_records_check 2714278a…: self-test OK, LEGACY 303 record(s) in 75 closed namespace(s), all intact.
• citation_roles_check 2714278a…: self-test OK, CITATIONS 0 manifest(s), 0 id(s), all hold.
• duplicate_check: OK.
• SC-42 integration check (bell-operational-reconciliation-20261029/check_sc42_integration.py): rc 0. The normal and -O outputs are byte-identical to sc42-integration-result.json, and --self-test is byte-identical to sc42-integration-controls.json.
• An observation outside this PR's scope: the older tracks/SC42-operational-kinematics/check_sc42.py does not reproduce its committed check_sc42.out at main d9f0a845, or at its own recording commit 6a4e1194. It is a working-tree-vs-base scanner whose output drifts as the tree moves. At this head its output differs from main's only in the scanned-chunk count, so neither new file adds any hit.

6. CI

• Run 42034997259 (verify, pull_request, head_sha 2714278a) concluded success: 25 jobs succeeded, including "Mathlib bridge" (its Build and Release gate steps succeeded) and "Lean kernel check". 1 job was skipped: the A42 exclusion matrix placeholder, which is also skipped on main runs.
• mergeable_state: clean; the PR is still a draft.
• This is a pull-request run, so it tested a synthetic merge, not a workflow_dispatch at exactly 2714278a. Because the base equals the head's parent, the merge tree is the head tree. Whether a dispatched exact-head run is also required is the owner's call; I dispatched nothing.

Optional nits (none blocking)

• O1. The §A.42 item 8 table lists only the evidence references. Either add rows for Introduction full-corpus scientific consistency audit (gate for #918) #941 c.6658967061 and c.6658728711 (authority: provenance) and for the staging branch, or title the table as covering the evidence references.
• O2. The comparator prints REPRODUCTION HOLDS (0 failure(s)) …, with two spaces (compare_result.py at 48b18ac5, line 303). The README quotes it with one space.
• O3. The staged README (O-4 at e73f7be3) notes that compare_result matches reports by declaration name and that R4 checks only the set of recorded lines, not which line each report sits on. Carrying that one-line limitation into the remediation route would serve a later reproduction.
• O4. Optionally, name the decision's author ("amaybaum") beside the date, as the PR body does.

No other writes were made: no push, dispatch, branch change or merge.

---

Generated by Claude Code

[amaybaum]

Merge record (owner approval #941 c.6660592367; standing integration rule)

Merged at integrated head 6e72df0cac4fb2338b6e8c24b8e1b57bfc0c1246 as the normal merge commit b28888ff1279579a6abb3c1ebbee9072d860c6d7, with parents 9f9dbc28 (main, after #1134 and its green main CI) and 6e72df0c.

1. Net content: git diff d9f0a845 2714278a is byte-identical to git diff origin/main 6e72df0c. It covers the two files of the retention record, introduction-repro-ext/README.md and results-121598983127-28.json. The results file keeps blob 97a2377d.
2. Clean integration: merging main 9f9dbc28 produced no conflicts. The README makes no reference to the Introduction's former Appendix A.
3. Scope check: duplicate_check, artifact_placement_check, staleness_check and coverage_check pass on the integrated tree.
4. Exact-head CI: PR run 42050582073 at 6e72df0c succeeded, with 25 jobs green and 1 matrix template skipped.
5. Freshness: the branch contained main (9f9dbc28), and main did not move before the merge.
6. No new permissions and no dispatches. evidence-replay.yml was not dispatched.
7. After the merge:
   • The merged tree equals the tree of 6e72df0c.
   • main CI verify run 42052526287 at b28888ff succeeded (25/25, 1 skipped).

Preserved per the owner's ruling:

• The staging branch staging/introduction-repro-ext-20261027 is still present.
• The workflow pin EXPECTED_28: e73f7be3… with EXPECTED_28_BLOB: 97a2377d… is unchanged.
• The workflow's dependency on the staged commit stays open under Introduction full-corpus scientific consistency audit (gate for #918) #941.

Retaining this file is not scientific acceptance of it.

---

Generated by Claude Code