[amaybaum]

Landing 3 of 3 in the owner-approved plan (amaybaum, Claude Code session chat, 2026-11-04: "Land the missing sources", then "Approve all three"). It was cut from main 9d022a65 and is now updated with main 5425dd02 (after #1097, #1098 and #1099). Its files are disjoint from theirs, but the evidence is not independent of #1099 (see below).

Head 27383a03: commit a025eb4e and one merge of main. The merge is an ordinary merge of main 5425dd02, for the up-to-date rule. It conflicts with nothing and changes none of this PR's files. The net diff against main is byte-identical to the reviewed 9d022a65..a025eb4e.

What it lands. Commit a025eb4e:

• Modules: three files copied byte-identically from Research (WIP): SUBSTATE-1 — internal sub-states and visible recurrence #1009's branch at 8af2d904 (unchanged at its head d4a80fc8):

  • OIBridge/ObservableFactorRecurrence.lean (92 lines, 2 axiom reports);
  • OIBridge/ObservableMeasureReturn.lean (115 lines, 2 axiom reports);
  • OIBridge/GradientLinkFlatness.lean (59 lines, 3 axiom reports).

  None contains sorry, admit, an axiom declaration, native_decide, unsafe or implemented_by. Their imports are RecurrenceHorizon and EquivalenceChain, both on main with the same blobs as on Research (WIP): SUBSTATE-1 — internal sub-states and visible recurrence #1009's branch, plus Mathlib.

• OIBridge.lean: three imports, placed after NativePadicReduction.

• lean-manuscript-census.json: Research (WIP): SUBSTATE-1 — internal sub-states and visible recurrence #1009's two kernel-only families for these modules, verbatim from 8af2d904, appended at the end. The census goes from 120 to 122 families; every other entry and key is unchanged.

Why. The observer-relative-finiteness dependency audit on main (DEPENDENCY-AUDIT.md) refers to #1009's work; these modules are its Lean part.

• :260, "Research (WIP): SUBSTATE-1 — internal sub-states and visible recurrence #1009 Lean candidate", is the measured exact observable return. ObservableMeasureReturn.measuredGamma_eq_one_iff proves both directions under positive, finite cell masses, using ObservableFactorRecurrence.
• :329–332, "Research (WIP): SUBSTATE-1 — internal sub-states and visible recurrence #1009's pure-gradient flatness/source failure", is the gauge-action control. The flatness half is GradientLinkFlatness.square_gradient_flat.

Dependence on #1099, which is now merged (5425dd02). The audit's #1009 rows are fully on main once this PR lands too:

• The "source failure" half of :329–332 is in native-link-sourcing-gate.md and native_wave_gradient_check.py.
• The solenoid control at :324 is in solenoid-countercontrol.md and solenoid_markov_probe.py.
• All four files are carried by evidence(§A.42, landing 2 of 3): copy the branch-only sources that records on main rely on #1099.
• evidence(§A.42, landing 2 of 3): copy the branch-only sources that records on main rely on #1099's copied notes (README.md:183–185, :261–264, equivalence-and-d3-scope.md:45–46) cite these modules in turn.

References inside the copied text (§A.42 item 8, adopted by #1097).

• ObservableMeasureReturn.lean:22–23 says it was "kernel-built on exact Research (WIP): SUBSTATE-1 — internal sub-states and visible recurrence #1009 head a02e197d" (CI 41094894776). evidence(§A.42, landing 2 of 3): copy the branch-only sources that records on main rely on #1099's copied notes (README.md:180–190, equivalence-and-d3-scope.md:45–47) say the same of both Observable modules.
  • Both modules changed after a02e197d, in Research (WIP): SUBSTATE-1 — internal sub-states and visible recurrence #1009 commit 798558b7: ObservableMeasureReturn +17/−12 lines and ObservableFactorRecurrence +6/−4. GradientLinkFlatness is unchanged.
  • The a02e197d build therefore attests an earlier version, and is provenance only.
  • The landed blobs are built and axiom-checked by this PR's exact-head CI and then by every main build.
  • The lines stay byte-identical here. Rewording them is item C of the approved correction PR, which will cite the build of this PR's landed head.
• The census notes' pointers to PR Research (WIP): SUBSTATE-1 — internal sub-states and visible recurrence #1009 and issue SUBSTATE-1: observer-relative finiteness without a finite-total-carrier requirement #1007 are provenance.

Scope.

• Evidence retention only; no proof is changed and no claim is promoted.
• The census notes keep Research (WIP): SUBSTATE-1 — internal sub-states and visible recurrence #1009's wording, which says the statuses depend on an exact-head Mathlib build. This PR's CI is that build on current main.
• If the build fails, the failure is reported and no proof is repaired.
• Research (WIP): SUBSTATE-1 — internal sub-states and visible recurrence #1009 stays open; if it merges later, it will find these files identical.

Checks (local).

• Census: the census tool passes. Its countercontrol, run on main's census plus the three modules, fails as expected with three UNCLASSIFIED modules.
• Other repository checks: placement, duplicate, claims and voice pass.
• Not run locally: the Lean build and axiom report. They run in CI (§A.40).
• Closing keywords: none in the commit message or this description.

Gates.

• Independent exact-head review, including the §A.42 item 8 trace. Review at a025eb4e: PASS, nothing blocking. The owner approved that head (amaybaum, session chat, 2026-11-04). For updated heads: "the previous exact-head approvals remain applicable only to those heads and their original gates. Updated heads require their own integration checks."

• Independent delta review of the update at 27383a03: CONFIRMED WITH NITS, nothing blocking. It confirmed that:

  • the parents are a025eb4e and 5425dd02;
  • the net diff is byte-identical to the reviewed one;
  • the merge equals the automatic merge, and main's 259 changed paths do not overlap this PR's 5;
  • OIBridge.lean and the census are the reviewed blobs: three imports, each once; 122 families, with no duplicate names or keys;
  • the three module blobs are those at a025eb4e, 8af2d904 and d4a80fc8.

  Its nit N1, that the copied text cites the off-main build at a02e197d, is covered above. Its nit N2 is that the PR stays in draft until the required checks are green at this head.

• Green CI at the exact head 27383a03, including the Mathlib bridge job's Build and Release gate steps.

• Owner approval naming the exact head SHA.

• Merge commit only.

🤖 Generated with Claude Code

https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

[amaybaum]

Merged. Merge commit 82f0e119fd32122c00716060bbe4e93e97fb05f8, pinned to head 27383a036d76bf4fd72a7a9f35b281af405630b4.

Owner approval (amaybaum, Claude Code session chat, 2026-11-04): "Once all required CI checks on 27383a03 pass, I conditionally approve its normal merge, provided the exact head, reviewed file delta and mergeability remain unchanged."

Conditions checked immediately before the merge:

• Head and base: the remote head was 27383a03 and the base was main 5425dd02.
• File delta: git diff --binary origin/main 27383a03 was byte-identical to the reviewed 9d022a65..a025eb4e.
• Mergeability: GitHub reported it mergeable and clean.
• CI: run 41869638020 at 27383a03 concluded success, with 25 checks succeeded and 1 skipped by design. In it, the Mathlib bridge job's Build, Release gate and axiom-report steps all concluded success, read from the run's job records.

After the merge:

• Ancestry: the parents are 5425dd02 and 27383a03, and the tree (6f7fa599) equals the head's tree.
• Diff: git diff 5425dd02 82f0e119 touches exactly the census, OIBridge.lean and the three modules.
• Census: tools/lean_manuscript_census.py passes on 82f0e119. It shows 122 families with no duplicate names, every module classified.
• main CI on 82f0e119 is running. Its run will be cited, once its Mathlib steps are confirmed, by the correction PR's item C as the build that checks the landed modules. The a02e197d build stays as provenance for an earlier version that differs only in doc comments.

No theorem, definition, proof or import was changed. #1009 is untouched.

---

Generated by Claude Code