[amaybaum]

Landed

Merged with separate owner approval as 7c1c2ae2ab404b8732aafe61201e09c1df3bb253, with ordered parents 6fa284a5f3a48ffb1cb9ee3a8dd13b129a3a7248 and approved head b2f059a2ce7f1a4e0da7077e487b9962f50e8c6d. Landing tree exactly matches reviewed 282afafc3e88b8b94c2b7bd6149a9784436fcb27. Main's post-merge CI 40836744661 passed 25 jobs with one expected skip. #991 is now separately reconciled at da66fc774d1bb76e6531d002f0d64f8bc6ab1eec, with its own CI/review/approval gates.

This PR adds the exact finite-image whole-future hidden-memory and capacity result, building on #990, now merged to main.

Current candidate: b2f059a2ce7f1a4e0da7077e487b9962f50e8c6d.
Reviewed source candidate: 28d29fad3ad0465d22e7829c37cad6e33ccde948.
Identical tree: 282afafc3e88b8b94c2b7bd6149a9784436fcb27.

The current candidate is an owner-authorized intentionally empty, single-parent child of the reviewed source candidate. GitHub comparison reports one commit and zero changed files. No proof, scientific content, control, entropy convention, scope, manuscript, coverage grade or workflow changed.

Current landing and CI checks

• Base is main 6fa284a5f3a48ffb1cb9ee3a8dd13b129a3a7248. Its push CI 40833111636 passed 25 jobs with one expected skip.
• Fresh ordinary synchronize PR CI 40835646719 passed: 25 successful jobs and one expected skip. Its run record names the current head and current main base.
• Fresh synthetic merge aee314232b3014e1b195c98954ae0519a1295942 has ordered parents current main and current candidate, and exactly the reviewed tree above.
• The scoped no-content-change confirmation follows from identical tree object IDs and the empty commit diff. The independent mathematical/scoped reconciliation ACCEPT applies to reviewed source 28d29fad and its unchanged tree; it is not presented as a newly performed full scientific review.
• Separate owner approval was received and the exact candidate was merged; the landing and post-merge CI are recorded above.

Preserved accepted scope

The exact entire visible sequence has a finite image because the initial product carrier is finite. Equality of codes is equivalent to coordinate equality at every future time, and actual orbit decoding is proved. Ordinary discrete Shannon conditional information in bits is taken on this finite image, for an arbitrary initial probability law and nonempty hidden space. The whole-future hidden-information/capacity bounds and genuine supremum over all natural times are preserved.

The theorem does not certify equality with a finite-prefix supremum, a separate infinite-product measure/limit entropy formulation, an N−1 bound, a physical retained-record mechanism or permanent hidden-state uncertainty. No blanket Main/K3 grade promotion is made.

Against #990's tree, the delta remains exactly the original six files (+345/−0). FullFutureMemory.lean, the written scope/entropy convention, controls and saved results are byte-identical to accepted checkpoint 96a3020be0add86ce916bdc103b4067cff79d5d1. Census/imports preserve #990 and the whole-future recovery. All manuscript sources, publications, coverage grades and workflows remain unchanged.

Source checkpoint verification and provenance

Independent scoped reconciliation review accepted 28d29fad and the unchanged tree: original six-file delta, unchanged five-module dependency cone/toolchain/mathlib pin, exact sequence-image construction and decoding, finite-image entropy convention, whole-future bound and genuine supremum.

At that source checkpoint, local census, coverage (133 canonical statements), staleness (13 matched), diff and source preservation checks passed. The controls replayed under normal and optimized Python with 13,344 exact coordinate predicates, two exact countercontrols and 478 numerical entropy checks (tolerance 10^-12); deliberate failing guards exited nonzero in both modes. These controls supplement the universal Lean proof.

Source checkpoint CI 40826550173 passed 25 jobs with one skip before retargeting. It is provenance, not the fresh post-retarget CI required above. Accepted 96a3020b passed 40731207990. Earlier checkpoints remain in history, including rejected assertion-based controls at 10c2a5a4.

The source, entropy convention and replay recipe are under verification/audits/manuscript/full-future-memory-20261028/. No manuscript/publication changed, so no canonical rebuild is required. No local Lean/release build, special workflow dispatch, native designation or merge occurred. #991, editorial corrections and Introduction #918 remain separate. Related: #961, #946.

[amaybaum]

Post-#990 merge dependency handoff

#990 merged as 6fa284a5f3a48ffb1cb9ee3a8dd13b129a3a7248; GitHub now reports this dependent PR targets main, while the original, independently accepted head remains 28d29fad3ad0465d22e7829c37cad6e33ccde948. Its exact-head PR CI passed 25 jobs with one expected skip; accepted whole-future image/entropy/time-supremum theorem and controls remain intact.

Compare against current main: 3 ahead/1 behind, merge base equal to #990's approved head 7a8f2714, because main has the additional merge commit. Re-check the proposed resulting tree, imports, census and full-future entropy scope. If any source or audit changes are necessary, obtain independent diff review and new exact-head CI before requesting separate owner approval. Do not silently promote beyond accepted proof grades or merge on the strength of #990's approval. Main's push CI at 6fa284a5f3a48ffb1cb9ee3a8dd13b129a3a7248 must also be confirmed green.

This is a planning note only; no branch/source changes performed.

[amaybaum]

Confirmed test-merge identity after #990 landing

Current main 6fa284a5f3a48ffb1cb9ee3a8dd13b129a3a7248. #993 still 28d29fad3ad0465d22e7829c37cad6e33ccde948, targeting main.

GitHub's current PR test-merge commit is c4fc5babd68e3b345de2f6968e62341ae2e28829. Comparing the accepted #993 head to that test merge shows one merge commit and ZERO changed files. Inspection of the test-merge census confirms both independent families TrajectoryMemory and FullFutureMemory, for 114 total. This is an exact proposed-tree consistency check; accepted 25-success/1-skipped PR CI run 40826550173 remains valid for its original head, and the full-future claims remain kernel-only.

Open gates: confirm green push CI at main's #990 merge commit; obtain explicit owner approval for #993 at the unchanged exact head if it is the next merge. If #991 lands first, re-run test-merge and census checks against the resulting main: the additional #991 families/imports will overlap and may need reconciliation, with renewed review/CI. No source/head modification or merge was made here.

[amaybaum]

Post-retarget CI gate — no source changes or merge authorized

Read-only verification: main's merge-commit run 40833111636 has 25 success / 1 expected skip. Current #993 remains draft at 28d29fad3ad0465d22e7829c37cad6e33ccde948, base main at 6fa284a5f3a48ffb1cb9ee3a8dd13b129a3a7248, mergeable, but the only PR-triggered run 40826550173 was prior to #990 landing.

The .github/workflows/verify.yml workflow triggers on pull_request, push to main, and workflow_dispatch. It runs on pull-request synchronize events for new PR head commits. Merely retargeting the base, reusing old CI, or rerunning the old attempt is not evidence that the current PR merge against new main was checked. A head-only workflow_dispatch also does not by itself test the PR merged context.

Recommended non-content-changing action for branch writer: produce one intentionally empty commit (git commit --allow-empty) on #993's existing branch and push it to trigger a genuine new pull_request.synchronize CI run against main. Re-confirm the new head's tree exactly matches reviewed 28d29fad, merge base is current main, no manuscript/audit/proof/grade files changed, independent scoped review accepts the empty change, and exact-new-head PR CI passes (25/1 expected). If the workflow cannot be triggered in this way, document the alternative event's checkout SHA and actual merge-tree test explicitly. Return the exact new SHA for separate owner merge approval; do not merge automatically. #991 remains independent and conflicted pending reconciliation.