[amaybaum]

This PR reconciles the accepted finite-trajectory hidden-memory and C3 capacity recovery with main 925d2f0ea4e7a1dc62c35d4ec5d8ef321788b116, after #994 and #995. Current candidate: 7a8f271401611d5d18d5818b64eaac7f266e8a1e (tree e827d51683dbee43a89a532986b08e2077f8b7b9). Main is unchanged by this PR until explicit owner merge approval.

The reconciliation is a normal merge commit with ordered parents a958bc5479cb9728b2f374fcd2b4873b8cdecbf7 and 925d2f0ea4e7a1dc62c35d4ec5d8ef321788b116. The original reviewed checkpoints remain in history. Against main, the delta is exactly the original three files: TrajectoryMemory.lean, its OIBridge import and its kernel-only census family. All accepted Lean proof bytes are unchanged; all manuscript sources, publications, 133 canonical statement grades and workflow files match main. No publication rebuild is needed for this code-only reconciliation.

Accepted mathematical scope preserved:

• Construct the time-t law from an arbitrary initial probability law and actual finite-permutation iterates; prove next-step and future-block joint-law transport.
• Apply hidden-memory and C3 bounds to the actual orbit variables.
• Bound the genuine supremum over every natural time/horizon pair and its per-process hidden-alphabet capacity.

This PR covers finite future blocks. The stronger exact whole-sequence finite-image result remains separately in dependent #993. No posterior opacity, physical retained-record mechanism, accumulation without hidden-state reuse, or manuscript/K3 promotion is claimed.

Verification of the reconciled candidate:

• Cheap local census, coverage (133 canonical statements), publication staleness (13 matched), diff and exact-source preservation checks pass.
• Fresh independent scoped reconciliation review: ACCEPT at this exact SHA/tree. A reviewer separate from the author checked the complete recovery delta, unchanged four-module dependency cone/toolchain/mathlib pin, actual-law construction, time indexing, finite-block bounds and genuine supremum. No scientific or provenance blockers; complete current CI remains required.
• Fresh normal automatic PR CI 40826414480 passed at this exact head: 25 successful jobs and one skipped, including the complete Mathlib job, Build and Release gate. Its synthetic merge tree exactly matches the published head tree. Independent scoped review and current CI are complete; explicit owner approval for a normal merge commit remains outstanding.
• Full Lean/Mathlib and release checks run in CI under AGENTS §A.40. No local Lean build, special dispatch, native F/E designation or merge was performed.

Earlier provenance remains snapshot-scoped: rejected compiler candidates and the header/type/iterate fixes stay in branch history; accepted a958bc54 passed 40727678567, 25 successful jobs and one skipped. These receipts do not replace verification of the new candidate.

Publication sequence: #990 first, #993 after #990, with #991 reconciled independently against main. Editorial audit and Introduction #918 remain separate. Request explicit owner approval only after independent review and complete green CI at the exact resulting SHA. Related: #946, #961, #982.

[amaybaum]

Post-#982 handoff — reconcile memory/C3 recovery before landing

Foundational PR #982 merged into main as dffe1945989f60632c75b2b3e2e96afad2af8509 (approved head 7ac361440e879f449aa108e127347544f932c83c). The recovery candidate on this PR remains a958bc5479cb9728b2f374fcd2b4873b8cdecbf7, draft and unmerged.

Current comparison to main: the history diverged from shared ancestor 20ca05fe; #990 is ahead by 3 commits and behind main by 5. GitHub reports it mergeable, but this does not substitute for source reconciliation or CI at the eventual landing tree.

Required before #990 merge approval:

1. Reconcile the accepted actual-trajectory finite-block proof source, imports, census and audit records onto current main without overwriting the Foundational reconciliation: integrate #992 and preserve recovered theorem scope #982 corrections or proof scopes. Preserve independent accepted review provenance and the historical CI receipt for its original exact head.
2. Keep the full infinite-future image theorem (WIP: exact finite-image whole-future memory and capacity #993) as a subsequent separate unit. Do not use WIP: exact finite-image whole-future memory and capacity #993's stronger result to silently upgrade WIP: actual trajectory bridge for hidden memory and C3 capacity #990's finite-block theorem or Main ledger grades.
3. Obtain independent diff/scientific review and exact-head CI on the resulting main-targeted WIP: actual trajectory bridge for hidden memory and C3 capacity #990 landing candidate. Separately confirm main's own merge-commit CI as required by the release policy.
4. Present the reconciled exact SHA for explicit approval. Do not merge this PR, WIP: exact finite-image whole-future memory and capacity #993, or Introduction Introduction paper: reconcile sources and integrate scoped theorem recoveries #918 automatically.

No changes to #990's source/head, no special dispatch, no additional PR merge in this handoff.

[amaybaum]

Exact-head merge record — #990

Authorization: owner instructed "Proceed as suggested" following approval to merge this specific candidate.

Pre-merge: main at 925d2f0ea4e7a1dc62c35d4ec5d8ef321788b116, #990 at 7a8f271401611d5d18d5818b64eaac7f266e8a1e, mergeable and unchanged. Fresh independent review ACCEPT at that source, verify run 40826414480 completed SUCCESS (25 passing jobs, 1 expected skip). Only three files differed: OIBridge/TrajectoryMemory.lean, its import in OIBridge.lean, and a kernel-only Lean-manuscript census entry.

Merge: marked ready and used normal GitHub merge method with GitHub's expected_head_sha guard. GitHub returned merged: true and merge commit 6fa284a5f3a48ffb1cb9ee3a8dd13b129a3a7248.

Post-merge checks: PR API reports merged/closed with that merge SHA. 6fa284a5...main compares IDENTICAL (current main points to this merge); 7a8f2714...6fa284a5 is one commit ahead with zero changed files (content/tree identity by compare). The pre-merge main and PR head are the expected normal merge parents; the connector's fetched-commit shape omits parent/tree metadata, so this record does not falsely claim to have independently read those raw objects.

Main CI: exact push verification on the new merge commit must still be confirmed. The available commit-to-workflow query filters to PR-triggered runs and returns no main-push run; original green PR CI cannot be substituted for merge-commit CI.

Next: #991 is currently divergent from newly merged main (5 ahead/5 behind from old base), and #993 is a dependent branch (3 ahead/1 behind from old #990 head). Reconcile without overwriting accepted Lean proofs, controls or review receipts. Main's post-merge CI must be confirmed before additional landing authorization. No other PR merged. Editorial issue #996 and Introduction #918 remain independent.

[amaybaum]

Merge record

• Merged as: 6fa284a5f3a48ffb1cb9ee3a8dd13b129a3a7248, a normal merge commit, owner-approved at exactly 7a8f271401611d5d18d5818b64eaac7f266e8a1e.
• Parents: 925d2f0ea4e7a1dc62c35d4ec5d8ef321788b116 (previous main) and 7a8f271401611d5d18d5818b64eaac7f266e8a1e (approved head).
• Tree: e827d51683dbee43a89a532986b08e2077f8b7b9, identical to the approved head's tree. 925d2f0e is reachable from main.
• Delta: OIBridge/TrajectoryMemory.lean (byte-identical to the accepted a958bc54), its OIBridge import, and a kernel-only census family. No manuscript, publication, grade or workflow change.
• Pre-merge evidence: exact-head PR CI run 40826414480 succeeded, and the scoped independent review accepted.
• Main push CI: run 40833111636 on 6fa284a5 completed with success.

Next:

• WIP: exact finite-image whole-future memory and capacity #993: retarget to main and run fresh CI.
• WIP: formalize nonempty record-fibre identification and recurrence bridges #991: reconcile the census-file conflict, then a fresh scoped review and exact-head CI.
• Each needs its own exact-SHA owner approval.

---

Generated by Claude Code