[amaybaum]

Minimal evidence landing for SUBSTATE-2 (accountable Issue #1010). Owner authorization: #1088 c.6631552211 (amaybaum, session chat, 2026-11-04, quoted verbatim there): "Land all 32 files byte-identically from #1011's reviewed head 947761dd. Add only the two necessary Lean imports and their census entries. Do not duplicate F2CoherenceControls, its import or census family, which are already on main." #1011 stays open; closing it is a separate owner step after the #1010 handoff.

Head

• Landing commit 5e8c496f2253aa4be05ca4159d9bebaf6a80f39a, single parent 2a978edc (then main).
• main moved to 8a47132d when evidence(MR-1, #866): land the five stage-1 records of #1023 #1095 merged, so the branch was updated by an ordinary merge, never a rebase: head 09dc83ae5301e06004091b4de41c5fa80bcd9e29, parents 5e8c496f and 8a47132d. The merge needed no conflict resolution.
• Net diff against main 8a47132d: 32 added files and 2 modified files, 6850 insertions, 0 deletions. This is the same patch as 5e8c496f against 2a978edc (equal patch-id).

Commit-message correction. The commit message of 5e8c496f says "the 15 F2-1 files". That count is wrong: 13 F2-1 files land. The commit message is not rewritten. The landing holds 32 unique files: 2 Lean modules and 30 records (5 at the top level of recursive-substates/, 7 in fixed-scale-skew/, 5 in native-padic-bridge/ and 13 in f2-1-coherence-sourcing/).

What lands

• 32 files absent from main, byte-identical to 947761dd40c17e4fdedcd8972a0b4e53e8bfba42 at the same paths:
  • verification/lean-mathlib/OIBridge/RecursiveFiniteFactor.lean and OIBridge/NativePadicReduction.lean;
  • 30 records under verification/programmes/substratum/recursive-substates/, as counted above. The F2-1 files include stage2/ (run 1) and stage2/run-2/.
• verification/lean-mathlib/OIBridge.lean: the imports OIBridge.RecursiveFiniteFactor and OIBridge.NativePadicReduction, after OIBridge.RootedRecurrenceBridge, as in 947761dd.
• verification/lean-manuscript-census.json: the two kernel-only SUBSTATE-2 families for those modules, verbatim from 947761dd and in its position (before the F2-1 family). 120 families; every other entry is as on main.

Not duplicated: OIBridge/F2CoherenceControls.lean (blob fbf47504), its import and its census family are already on main, identical, via #1089 (4312028a).

Dependencies this addresses (§A.42 item 2)

• PC-1 (records on main via evidence(PC-1): retain PC-1's records and kernel controls on main (D-72) #1089) cites the F2-1 preregistration, A★, its stage-2 records, NATIVE-PADIC-1 and the recursive README models, which until now existed only on research: SUBSTATE-2 recursive inverse-limit substructure and depth-feedback controls #1011's branch.
• MR-1 (records on main via evidence(MR-1, #866): land the five stage-1 records of #1023 #1095, merge 8a47132d) cites the F2-1 run-2 record at 4e7ddb70.

After this lands, that content is on main in its 947761dd form, which differs from the pinned commits in four records:

• README.md, native-padic-bridge/REPORT.md and fixed-scale-skew/REPORT.md differ from both 4e7ddb70 and c811e876. The changes replace wording that independent review was pending with the author-reported re-review and its unresolved reviewer provenance. README.md also adds a pointer to the post-closeout G★ correction (#1011 c.6546748788), which states that the thirteen-rule outcome is unchanged.
• run-2/RESULT.md differs from 4e7ddb70 in one line: "Independent exact-head review" reads "Author-reported independent exact-head review".

No verdict or result differs.

Branch-only commits (provenance; none is on main)

On research/substate-2-recursive-20261030, kept at 947761dd:

Commit	Role	Cited by
66eb48ca	F2-1 preregistration freeze (guards the non-transplantable disjunct; no execution)	F2-1 records in this landing; PC-1 preregistration and vendored run-2/controls.py; F2CoherenceControls.lean and its census family on main
b86f0547	F2-1 stage 1: A★ delta review closed (no execution)	the same
fdeeb2d5	F2-1 A★-1 review edits (no build)	F2-1 records; PC-1's vendored run-2/controls.py
05ecc873	F2-1 stage 2 run 1: controls only, owner-authorized; its outcome is VOID	F2-1 records; PC-1 PC-S2.md, stage2/RESULT.md, vendored run-2/controls.py
1d345126	F2-1 stage 2 run 2: bounded proof repairs, statements byte-identical; INCONCLUSIVE (gap) confirmed at this head	F2-1 records; PC-1 preregistration and PC-S2.md
2155273f	F2-1 run 2: exact-head CI evidence and token recorded	F2-1 run-2/RESULT.md
4e7ddb70	F2-1 run 2: final review and two record corrections; the F2-1 record PC-1 and MR-1 pin	PC-1 and MR-1 preregistrations, stage1-log.json, PC-S2.md, MR-star.md; PC-1 stage2/RESULT.md, stage2/controls.py and stage2/run-2/controls.py
c811e876	SUBSTATE-2 review fixes; the SUBSTATE-2 source PC-1 pins for NATIVE-PADIC-1	PC-1 preregistration; records in this landing
947761dd	#1011's reviewed head and the source of every landed byte	this PR

On research/substate-1, not touched by this landing:

Commit	Role	Cited by
b40ba681, 35055d31	SUBSTATE-1 wave-torus probe (visible recurrence; scoped claims)	native-padic-bridge/REPORT.md in this landing, as provenance only
8af2d904	SUBSTATE-1 later-access result review; native apparatus constructions	PC-1 PC-star.md (Q10), MR-1 MR-star.md, preregistration and stage1-log.json. It stays branch-only; this landing does not address it

The 'Cited by' column lists the main citing records, not every one. The frozen records keep citing these commits. Both branches are kept.

Scope

Evidence retention only. No scientific status changes and no proof changes.

• F2-1 run 1 keeps its VOID outcome. Correction to the commit message's wording: run 1's own stage2/RESULT.md records "Token. None yet"; the VOID outcome is recorded in run-2/RESULT.md, run-2/PROOF-REPAIRS.md and run-2/results.json. No record is edited.
• F2-1 run 2 keeps INCONCLUSIVE (gap) for the 13 screened rules.
• Reviews: the historical independent reviews remain author-reported, and reviewer provenance is unrecovered. Nothing is promoted. SUBSTATE-2: recursive inverse-limit substructure, depth feedback and gauge/quantum controls #1010's durable re-review gate, F2/L3 (OI ↔ QM equivalence: proof gate (dependency index; carries #885) #914) and P0: physical observable carrier and evolution selection #866 are unaffected.
• Limitations stand as recorded:
  • the compactness → finite-stage factor step is paper-only;
  • RecursiveFiniteFactor assumes the factorization and a supplied exact period;
  • NativePadicReduction covers the projection identities only, and the inverse property is unproved;
  • the FIXED-SCALE-1 infinite statement is not kernel-checked.
• Census notes: they are verbatim from 947761dd. Their sentence "The module builds and its axiom report passes in CI" describes research: SUBSTATE-2 recursive inverse-limit substructure and depth-feedback controls #1011's CI run (41284458598, against the 2026-11-01 main). This PR's CI is what re-establishes it on current main.

Checks

• Local static checks pass at the head 09dc83ae:
  • byte identity 32/32;
  • census tool, with a countercontrol that fails as expected without the two families (run at 5e8c496f; both edited files have the same blobs at the head);
  • artifact placement, migration manifest, claims, duplicate and voice;
  • staleness, coverage, dependency labels, mirror, citation, architecture and toolchain;
  • legacy records, citation roles and V3 receipts.
• Not run locally: the Lean build and axiom report (CI only, §A.40). Probe replays are out of scope.
• The independent review predicted a green Lean build. That prediction is not a substitute for CI. If the build fails, the failure is reported and no proof is repaired here.

Gates before merge

• Independent exact-head review: done at 09dc83ae, CONFIRMED WITH NITS. Both nits concerned this description and are applied here; there were no blocking findings.
• Green CI at the exact head.
• Owner approval naming the exact head SHA.
• Merge commit only.

🤖 Generated with Claude Code

https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb