[amaybaum]

Leftover outdated provenance lines noted by the exact-head review of #1107, fixed before #1088 closes.

Owner decision (amaybaum, Claude Code session chat, 2026-11-04), on the leftover lines: "Fix before closing". Standing limits: no deletions, no frozen-record changes, no scientific change.

Head

32c869552792501ff7eaf732af493f6034f1bf20, single parent 449b8fa8 (current main). Three files, four lines; line counts unchanged.

Changes in verification/programmes/substratum/recursive-substates/

File:line	Was	Now	Checked against main
README.md:80	"conditional Lean theorem candidate"	"conditional Lean theorem module"	OIBridge.RecursiveFiniteFactor imported at OIBridge.lean:25, census kernel-only; the same paragraph already says it builds and its axiom report passes in CI.
README.md:201	"A new research Lean candidate,"	"A research Lean module,"	OIBridge.NativePadicReduction imported at OIBridge.lean:26; the paragraph already says kernel-only, builds, axiom report passes.
native-padic-bridge/REPORT.md:3	"issue #1010 / draft PR #1011."	"issue #1010; landed on main by #1096 (#1011 closed unmerged)."	Added by 5e8c496f, which entered main through #1096.
fixed-scale-skew/REPORT.md:3	"Related to SUBSTATE-2 issue #1010 and draft PR #1011."	"Related to SUBSTATE-2 issue #1010; landed on main by #1096 (#1011 closed unmerged)."	Same.

The scope sentences around each module ("explicitly conditional", "proves … given finite-stage hypotheses", "The inverse property is not proved there", etc.) and the REPORT status texts, including fixed-scale-skew's "author-reported" re-review qualification, are unchanged.

Not changed

The three preregistrations that name draft PR #1011 (fixed-scale-skew/PREREGISTRATION.md:3, native-padic-bridge/PREREGISTRATION.md:3, f2-1-coherence-sourcing/preregistration.md:4) record where each was registered before its computation, which remains true; F2-1's preregistration is frozen. They are left as written. If the owner wants those lines changed too, that is a separate decision.

Local checks at the head

legacy_records_check.py: 303 records intact. citation_roles_check.py, duplicate_check, staleness_check, artifact_placement_check, lean_manuscript_census, voice_check, claims_check: exit 0.

Still needed before merge

Independent exact-head review, CI at the exact head, and separate owner merge approval of the reviewed SHA.

---

Generated by Claude Code

[amaybaum]

Merged. Merge commit e1d044d0e61d7c7e48aca9ab76e81fc0a2176737, pinned to head 32c869552792501ff7eaf732af493f6034f1bf20.

Owner approval (amaybaum, Claude Code session chat, 2026-11-04): "I approve a normal merge at that exact SHA, conditional on the head and mergeability remaining unchanged." Immediately before the merge the remote head was still 32c86955, the base main 449b8fa8, and GitHub reported the PR mergeable and clean.

Before the merge: exact-head review ACCEPT, no blockers; CI run 41902080208 at the head concluded success (25 succeeded, 1 skipped by design; Mathlib bridge Build and Release gate succeeded).

After the merge:

• The parents are 449b8fa8 and 32c86955, and the tree (b5b0d322) equals the head's tree.
• git diff 449b8fa8 e1d044d0 changes the four reviewed lines in three files and equals the reviewed diff.
• legacy_records_check.py at e1d044d0: 303 records in 75 closed namespaces, all intact.
• main CI on e1d044d0: push run 41904015801 concluded success; 25 checks succeeded and 1 was skipped by design. In the Mathlib bridge job, Build and Release gate both succeeded.

Noted by the review, left as is: native-padic-bridge/PREREGISTRATION.md:3 reads "Active research-only under issue #1010 / draft PR #1011"; it is a preregistration and is not rewritten after its outcome. f2-1-coherence-sourcing/stage2/RESULT.md:15 ("host PR #1011") belongs to F2-1's frozen unit.

---

Generated by Claude Code