[amaybaum]

Draft. Merge not authorized; no dispatch authorized. The owner decides on the exact reviewed SHA separately. Authority: owner decision #941 c.6658483078; plan c.6658442142.

Problem

.github/workflows/evidence-replay.yml pins EXPECTED_14: 4a260ca9…, which is #918's head. That commit is not reachable from main; it exists only on #918's branch and refs (#941 c.6658258907). The expected result it carries, blob 61cfd6ea at papers/introduction_repro/results-121598983127.json, landed on main with #1124 (merge f5efa7a0).

Change (head 0a07d8a9, two commits on main 13ced581)

• 528966ff: EXPECTED_14: 4a260ca9d6414e4d504a629ba5a0eb3c70bd4704 → EXPECTED_14: f5efa7a0813218b580272f7fd80a6b0c87eb6657, with the matching header comment.
• 0a07d8a9: the comment says "first pinned at Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's head 4a260ca", per review nit N1. It is a comment-only change.
• Unchanged:
  • EXPECTED_14_BLOB (61cfd6ea…);
  • the checks at :88 and :90 that read it;
  • the 14-module comparison;
  • every other pin. EXPECTED_28 (e73f7be3) is untouched, per the owner's decision.

Verification

• Independent review: ACCEPT (c.6658681447). It confirmed:
  • f5efa7a0:<path> = 61cfd6ea…;
  • f5efa7a0 is an ancestor of main;
  • a simulation of the workflow's retrieval and blob steps (:73–:91), run exactly as written in a repository with branches and tags only, passed every step. expected-14.json re-hashes to 61cfd6ea, with 14 modules; expected-28 still resolves only through the staging branch.
• PR CI on 528966ff: run 42031085409 succeeded.
• Pending: a delta check of 0a07d8a9 and CI at that head.
• evidence-replay.yml runs only on workflow_dispatch. A dispatch to confirm lean-fresh-build end to end would need separate owner approval.

Out of scope, noted by the review

verification/audits/manuscript/foundational-release-20261028/candidate-inputs.json:6 pins the workflow's old sha256. It is a point-in-time candidate record whose other hashes already differ from main. No tool reads it, and it is not a legacy record. It is left unchanged.

🤖 Generated with Claude Code

https://claude.ai/code/session_011zDyUSyEszk3JJx83uXKKq

[amaybaum]

Independent review of 528966ffa4d641e9a4075ab2e3a4c6f167cf9bdf: ACCEPT (one optional comment-wording nit, N1 below)

Scope: owner decision #941 c.6658483078, item EXPECTED_14. Checked on a fresh, non-shallow git clone --no-local, with no alternates and all refs/pull/*/head fetched. main was 13ced581 and the branch head 528966ff, both confirmed by ls-remote at review time. Nothing was dispatched, committed or pushed. The clone has been deleted.

1. Diff (13ced581..528966ff, one commit, single parent 13ced581)

• Only .github/workflows/evidence-replay.yml changes (+4 −3).
• env: only EXPECTED_14 changes, 4a260ca9d6414e4d504a629ba5a0eb3c70bd4704 → f5efa7a0813218b580272f7fd80a6b0c87eb6657.
• EXPECTED_14_BLOB (61cfd6ea…), EXPECTED_28 (e73f7be3…), EXPECTED_28_BLOB (97a2377d…), LEAN_COMMIT (17b830bc…), ARCHIVE_COMMIT (48b18ac5…) and BH_COMMIT are byte-unchanged.
• The rest of the diff is the header comment (ll. 13–16): the new wording, plus one re-wrapped line ("A step fails unless lake built every OIBridge module in the source"), whose words are unchanged.
• No step, trigger, permission or job changed. The YAML parses (yaml.safe_load).

2. The pin

• git rev-parse f5efa7a0:papers/introduction_repro/results-121598983127.json = 61cfd6ea2df4590cc2ff86f90fc8f50ab71201f7 = EXPECTED_14_BLOB. The path gives the same blob at 4a260ca9 and at main 13ced581.
• git merge-base --is-ancestor f5efa7a0 origin/main: yes. f5efa7a0 is the #918 landing: the Introduction (five files + six ledger rows), with the SC-42 REST allowance #1124 merge, on main's first-parent chain.
• For comparison, 4a260ca9 is not an ancestor of main. e73f7be3 is not either, and only staging/introduction-repro-ext-20261027 (head 0a8f4930) contains it.

3. Simulated retrieval and blob steps (workflow :73–:91, run exactly as written, with the new pin)

I built a repository holding only branches and tags, which is what actions/checkout with fetch-depth: 0 provides, with no refs/pull/*. Its origin was https://github.com/amaybaum/incompleteness and it was detached at 528966ff. I exported the env values from the PR head's file (ll. 48–54) and set a scratch RUNNER_TEMP. Lean, elan, the build and the gate were not run.

Step	Exit
git cat-file -e LEAN_COMMIT / ARCHIVE_COMMIT / EXPECTED_14 (f5efa7a0) / EXPECTED_28 (e73f7be3)	0 / 0 / 0 / 0, so no git fetch was needed for any of them
git update-ref refs/remotes/origin/main "$LEAN_COMMIT"	0
git worktree add --detach "$RUNNER_TEMP/dir" "$LEAN_COMMIT"	0
test "$(git -C … rev-parse HEAD)" = "$LEAN_COMMIT"	0
test ! -e …/verification/lean-mathlib/.lake	0
git show "$ARCHIVE_COMMIT:…/extract_result.py" and …/compare_result.py	0, 0
:88 test "$(git rev-parse "$EXPECTED_14:…json")" = "$EXPECTED_14_BLOB"	0
:89 the same for EXPECTED_28	0
:90 git show "$EXPECTED_14_BLOB" → expected-14.json	0. It is 64,105 bytes, re-hashes to 61cfd6ea, and holds 14 modules.
:91 git show "$EXPECTED_28_BLOB" → expected-28.json	0. It is 114,828 bytes, re-hashes to 97a2377d, and holds 28 modules.

So EXPECTED_14 now resolves from main alone. EXPECTED_28 still resolves only because the staging branch exists; this PR leaves that unchanged, as decided. This is a retrieval check only. Whether the lean-fresh-build job succeeds end to end is not established without a separately authorized dispatch.

4. Other references to the old value

• Mutable files at the head: git grep 4a260ca finds only evidence-replay.yml:15, the new header's "first carried at Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's head 4a260ca" (N1). No other file references EXPECTED_14, EXPECTED_28 or their values.
• Frozen or historical records: verification/audits/manuscript/foundational-release-20261028/candidate-inputs.json:6 pins evidence-replay.yml by sha256 (240b97e1…). That is the file at main 13ced581; at 528966ff it hashes to 866a2548…. That file is a point-in-time pin of that candidate's inputs, not a live invariant. Its AGENTS.md and verify.yml entries already differ from main, and no tool or check reads it, since the only reference is its own README:37. No edit is proposed.
• legacy-records.json does not list it.

5. PR CI (verify, pull_request)

Run 42031085409, attempt 1, head_sha 528966ff: status: completed, conclusion: success. Of 26 check runs, 25 are success and 1 is skipped. The skipped one is the unexpanded matrix placeholder "Numerical probes / A42 exclusion (${{ matrix.part }})". Mathlib bridge (the release gate), Lean kernel check and the aggregate Numerical probes are all success. This run tests the synthetic merge with main 13ced581. It is not an exact-head attestation and is not needed as one for this unit. evidence-replay.yml itself is workflow_dispatch-only and did not run.

Findings

• N1 (optional, comment wording only). "first carried at Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's head 4a260ca" is not accurate as history. Blob 61cfd6ea first appears on Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's branch at 3941ef88. The file was added at ed3ca911 as bd8630fc. On main, the blob first enters through 40fc5954, under f5efa7a0. 4a260ca9 is where the workflow first pinned it. "first pinned at Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's head 4a260ca" would be exact. This is not load-bearing, and no check reads it. Fixing it means a new head, with re-review and CI.
• No blocking findings. The change is the minimum one the owner's decision describes. It preserves the verified blob, and it makes the EXPECTED_14 path rest on main (§A.42 items 2–3).

Merge and any evidence-replay.yml dispatch remain separately gated owner decisions. This review grants neither.

---

Generated by Claude Code

[amaybaum]

Delta check 528966ff → 0a07d8a95b44e4b4dcfcd1dc212823af4e5e82d9: ACCEPT

1. Diff. One commit, single parent 528966ff; the branch history is 0a07d8a9 → 528966ff → 13ced581. The workflow file at both commits differs only on line 14, where "first carried at Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's head" became "first pinned at Introduction paper: reconcile sources and integrate scoped theorem recoveries #918's head". That is +1 −1 in .github/workflows/evidence-replay.yml, and no other file changed. The file's blob went from 8f25d986 to 3ee00491. No pin, step or check moved. The env at 0a07d8a9 is: EXPECTED_14 f5efa7a0…, EXPECTED_14_BLOB 61cfd6ea…, EXPECTED_28 e73f7be3…, EXPECTED_28_BLOB 97a2377d…, LEAN_COMMIT 17b830bc…, ARCHIVE_COMMIT 48b18ac5…, BH_COMMIT eae01647…. This resolves N1 exactly.
2. YAML. yaml.safe_load parses the file at 0a07d8a9.
3. PR CI. verify run 42032870420 (pull_request, attempt 1, head_sha 0a07d8a9) has status: completed and conclusion: success. Of 26 check runs, 25 are success, including Mathlib bridge, Lean kernel check and the aggregate Numerical probes. The other one, the unexpanded matrix placeholder "A42 exclusion (${{ matrix.part }})", is skipped, as on the previous head. This run tests a synthetic merge; it is not an exact-head attestation.

My findings in the earlier review (c.6658681447) all carry over to this head unchanged. Merge and any evidence-replay.yml dispatch remain separate owner decisions.

---

Generated by Claude Code

[amaybaum]

Owner merge approval (amaybaum, Claude Code session chat, 2026-11-05; quoted under §A.42 item 7):

Approve merging #1129 at 0a07d8a

Integration checkpoint.

• Why a new head was needed: main moved to d9f0a845 (Main: retitle the subtitle to 'Finite-Observer Representations and Quantum Reconstruction' (minimum change) #1130) after 0a07d8a9 was built on 13ced581. Branch protection requires the branch to be up to date, so a merge at 0a07d8a9 itself would be refused.
• New head: 51b020d3, a merge of main d9f0a845 into 0a07d8a9.
• Content check: the net change against main is byte-identical to the reviewed change, cmp <(git diff 13ced581 0a07d8a9) <(git diff d9f0a845 51b020d3). It is the one workflow file, and the YAML parses.
• Next: PR CI on 51b020d3. Under the standing rule, nothing is merged at a head other than the one approved, so 51b020d3 goes back to the owner for confirmation once CI is green.

---

Generated by Claude Code

[amaybaum]

Owner standing rule and conditional approvals (amaybaum, Claude Code session chat, 2026-11-05; quoted under §A.42 item 7):

1. #1129 — Conditional merge approved. Authorize merging PR #1129 at integrated head 51b020d3, provided: PR CI passes on that exact head. Its net diff against current main is byte-identical to the previously reviewed and approved change. No additional files, workflow behavior or scientific content changed. The PR is mergeable, and main has not changed since the final integration check. Use a normal merge commit, verify the merged tree, check main CI and record the result. Do not dispatch evidence-replay.yml. That requires separate approval.

2. Standing rule for content-identical integrations. For PRs that already have explicit owner merge approval, authorize the coordinating session to merge an updated integration head without requesting another approval, provided all of the following hold: 1. The previously approved net content change remains byte-identical. 2. The integration introduces no conflicts, relevant behavioral changes or new scientific dependencies. 3. An integration check confirms the approved scope and review remain applicable. 4. All required CI checks pass on the exact integrated head. 5. The branch is up to date and main remains unchanged immediately before merging. 6. No new permissions, scientific conclusions, workflow dispatches, freezes or execution authorizations are introduced. 7. The merge uses a normal merge commit, followed by merged-tree verification and main CI. If any condition fails, stop and request fresh review or owner approval.

3. #1131 — Conditional merge approved. I also approve merging #1131 once it has been integrated with current main, provided the same safeguards are met. Preserve the independently accepted six-file content change at e35ce775. Do not introduce the optional wording adjustment. If the integration changes relevant content or creates unexpected interactions, return for review rather than merging.

4. Scope of this policy. This policy applies only to PRs with explicit owner merge approval, including the two approvals above. It does not authorize merging every reviewed PR, nor does ACCEPT from an independent reviewer substitute for owner merge approval. Research PRs, scientific-status changes and any PR whose content differs from the approved version still require their applicable separate decisions. Record the integrated SHA and verification evidence for every merge.

---

Generated by Claude Code

[amaybaum]

Merge record (standing integration rule, c.6659123095)

Merged at integrated head 51b020d3d7e50a3a76aea85feafe0179dc802387 as a normal merge commit, 8418ec342420e6921808b4b6d9352f4857afd292. Its parents are d9f0a845 (main) and 51b020d3.

Conditions checked immediately before merging:

1. Net content. git diff 13ced581 0a07d8a9 is byte-identical to git diff origin/main 51b020d3. The only change is .github/workflows/evidence-replay.yml (+4/−3).
2. No conflicts or behaviour change. The integration merged main cleanly.
3. Scope. The diff is confined to EXPECTED_14 and its header comment. EXPECTED_14_BLOB and EXPECTED_28 are unchanged.
4. Exact-head CI. PR run 42034739875 at 51b020d3 succeeded: 25 checks passed and 1 matrix template was skipped.
5. Branch and base current. git ls-remote gave head 51b020d3 and main d9f0a845 just before the merge.
6. Permissions and dispatches. No new permissions. No dispatch, and in particular evidence-replay.yml was not dispatched.
7. After the merge.
   • The merged tree c8b348e6 equals the tree of 51b020d3.
   • main CI verify run 42037115788 at 8418ec34 concluded success.

The head branch was deleted automatically on merge. Its commits remain reachable as the merge's second parent.

---

Generated by Claude Code