diff --git a/verification/audits/manuscript/full-future-memory-20261028/README.md b/verification/audits/manuscript/full-future-memory-20261028/README.md
new file mode 100644
index 000000000..1d549c1d3
--- /dev/null
+++ b/verification/audits/manuscript/full-future-memory-20261028/README.md
@@ -0,0 +1,67 @@
+# Whole-future memory companion
+
+Research candidate, not yet independently accepted or compiler verified. Based on
+the accepted finite-block trajectory recovery at PR #990, `a958bc54`.
+
+## Exact object and entropy convention
+
+Let the finite initial sample space be Ω = V × H, with arbitrary normalized law μ,
+and let φ permute Ω. Define F(s)(j) = πV φ^(j+1)(s), for every natural j. The
+codomain FutureTrace is **the image of F**, a finite set of entire sequences. It
+is finite because F has finite domain. It can have fewer elements than Ω.
+
+At time t the whole-future random variable is Y_t(q) = F(φ^t(q)). Its j-th decoded
+coordinate is exactly X_(t+j+1)(q), not a finite-prefix approximation. Two codes
+are equal exactly when their decoded sequences agree at every future time.
+Every finite future block is a deterministic truncation of this same variable.
+
+The entropy convention here is ordinary discrete Shannon entropy of Y_t on its
+finite image, and similarly for its finite joint laws with X_<t and X_t. This is
+the literal entire-future variable for this finite deterministic realization.
+No infinite-product measure, sigma-algebra conditional entropy, limit theorem,
+or identification with a separate measure-theoretic convention is formalized.
+
+## Written proof
+
+Y_t is a deterministic function of (X_t,H_t), while the time-t joint law is the
+pushforward of μ along q ↦ (X_<t(q),φ^t(q)). Therefore the existing finite Shannon
+data-processing theorem applies to the actual entire-future variable:
+
+Iμ(X_<t;Y_t | X_t) ≤ Iμ(X_<t;H_t | X_t) ≤ log₂|H|.
+
+The bound holds for every natural t. The range of these conditional information
+values is nonempty and uniformly bounded above. Hence its genuine real supremum
+I*whole satisfies I*whole ≤ log₂|H|, and exponentiation gives 2^I*whole ≤ |H|.
+No replacement of a supremum by a finite maximum is made.
+
+This argument needs neither a period bound nor a claimed N−1 distinguishing
+horizon. It does not prove that a chosen finite prefix already determines the
+entire future. It does not derive a physical preparation, measurement or retained
+record, hidden-state opacity, or information accumulation without hidden reuse.
+
+## Relation to the manuscripts
+
+Main §3.4's C3 proof explicitly treats X_>t as a function of (X_t,H_t), but does
+not specify an infinite-product entropy convention. Under the finite-image
+discrete convention stated above, the companion matches that whole-future
+argument and the supremum over natural times. Any broader stochastic-process or
+measure-theoretic reading remains a separate dependency, not a silent promotion.
+No manuscript, coverage grade or prior accepted source is changed here.
+
+## Verification path
+
+The new module is imported by OIBridge's normal CI build and has a kernel-only
+research entry before the preserved final KTOKEN census family. Eight endpoint
+axiom reports are printed. No local Lean/Mathlib build or full suite is run under
+AGENTS A.40. The bounded independent controls use complete permutation-period
+words to encode entire traces in finite examples, with nonuniform/correlated
+initial laws, a short-prefix countercontrol, and sharp cyclic-register examples.
+Coordinate and degeneracy checks are exact; the Shannon entropy bounds and
+saturation checks are numerical with tolerance 10^-12. Explicit failure guards
+execute under normal and optimized Python; a deliberate failing guard must exit
+nonzero under both. These examples are controls, not universal proof certificates.
+
+The initial control checkpoint `10c2a5a4` used Python assert statements, which
+optimized Python removes. Its matching optimized output was not evidence of
+executed optimized checks. That rejected control revision is preserved in branch
+history; this correction does not alter the Lean module or written mathematics.
diff --git a/verification/audits/manuscript/full-future-memory-20261028/controls-result.json b/verification/audits/manuscript/full-future-memory-20261028/controls-result.json
new file mode 100644
index 000000000..15a18ab1d
--- /dev/null
+++ b/verification/audits/manuscript/full-future-memory-20261028/controls-result.json
@@ -0,0 +1,33 @@
+{
+  "status": "pass",
+  "checks": 13824,
+  "check_kinds": {
+    "exact_coordinate": 13344,
+    "exact_countercontrol": 2,
+    "numerical_entropy": 478
+  },
+  "permutations": 24,
+  "initial_laws": 3,
+  "saturation": [
+    {
+      "hidden_bits": 1,
+      "whole_future_cmi_bits": 1.0
+    },
+    {
+      "hidden_bits": 2,
+      "whole_future_cmi_bits": 2.0
+    },
+    {
+      "hidden_bits": 3,
+      "whole_future_cmi_bits": 3.0
+    },
+    {
+      "hidden_bits": 4,
+      "whole_future_cmi_bits": 4.0
+    }
+  ],
+  "kind": "bounded controls, not universal proof",
+  "optimized_output_identical": true,
+  "forced_failure_rejected_in_both_modes": true,
+  "control_sha256": "4fbc6cb726141ac129109f2d9632f3d4efdbeb65ffb7adae2707e09d8132ab66"
+}
diff --git a/verification/audits/manuscript/full-future-memory-20261028/controls.py b/verification/audits/manuscript/full-future-memory-20261028/controls.py
new file mode 100644
index 000000000..6c2ada34d
--- /dev/null
+++ b/verification/audits/manuscript/full-future-memory-20261028/controls.py
@@ -0,0 +1,104 @@
+#!/usr/bin/env python3
+"""Bounded controls for exact whole-trace entropy; not a universal proof."""
+from collections import defaultdict
+from fractions import Fraction
+from itertools import permutations
+from math import lcm, log2
+import json
+import sys
+
+
+def advance(p, q, n):
+    for _ in range(n):
+        q = p[q]
+    return q
+
+
+def order(p):
+    seen, period = set(), 1
+    for q in range(len(p)):
+        if q in seen:
+            continue
+        s, length = q, 0
+        while s not in seen:
+            seen.add(s)
+            length += 1
+            s = p[s]
+        period = lcm(period, length)
+    return period
+
+
+def entropy(weights, variables):
+    law = defaultdict(Fraction)
+    for q, w in enumerate(weights):
+        law[tuple(v[q] for v in variables)] += w
+    return -sum(float(w) * log2(float(w)) for w in law.values() if w)
+
+
+def cmi(weights, past, now, other):
+    return (entropy(weights, [past, now]) + entropy(weights, [now, other])
+            - entropy(weights, [now]) - entropy(weights, [past, now, other]))
+
+
+def variables(p, visible, t):
+    period = order(p)
+    past = [tuple(visible(advance(p, q, j)) for j in range(t)) for q in range(len(p))]
+    current = [advance(p, q, t) for q in range(len(p))]
+    now = [visible(s) for s in current]
+    # Periodicity makes each entire sequence exactly this finite cyclic word.
+    whole = [tuple(visible(advance(p, s, j + 1)) for j in range(period)) for s in current]
+    return past, now, whole, current
+
+
+counts = {'exact_coordinate': 0, 'exact_countercontrol': 0, 'numerical_entropy': 0}
+
+
+def require(condition, kind, message):
+    """Execute checks under normal and optimized Python alike."""
+    counts[kind] += 1
+    if not condition:
+        raise RuntimeError(message)
+
+
+if '--failure-control' in sys.argv:
+    require(False, 'exact_countercontrol', 'deliberately failed guard')
+
+for p in permutations(range(4)):
+    for weights in ([Fraction(1, 4)] * 4,
+                    [Fraction(x, 10) for x in (1, 2, 3, 4)],
+                    [Fraction(1), Fraction(0), Fraction(0), Fraction(0)]):
+        for t in range(2 * order(p) + 1):
+            past, now, whole, current = variables(p, lambda s: s // 2, t)
+            hidden = [s % 2 for s in current]
+            iwhole, ihidden = cmi(weights, past, now, whole), cmi(weights, past, now, hidden)
+            require(-1e-12 <= iwhole <= ihidden + 1e-12 <= 1 + 2e-12,
+                    'numerical_entropy', 'whole-future information bound')
+            for q in range(4):
+                for j in range(2 * order(p) + 1):
+                    require(whole[q][j % order(p)] == advance(p, q, t + j + 1) // 2,
+                            'exact_coordinate', 'actual future coordinate')
+
+# Identity retains hidden degeneracy in the whole trace: not an injective state code.
+p = tuple(range(4))
+_, _, whole, _ = variables(p, lambda s: s // 2, 0)
+require(whole[0] == whole[1] and whole[2] == whole[3] and whole[0] != whole[2],
+        'exact_countercontrol', 'identity keeps hidden degeneracy')
+
+saturation = []
+for bits in range(2, 6):
+    count = 2 ** bits
+    p = tuple(((s << 1) % count) + (s >> (bits - 1)) for s in range(count))
+    past, now, whole, _ = variables(p, lambda s: s >> (bits - 1), bits - 1)
+    info = cmi([Fraction(1, count)] * count, past, now, whole)
+    require(abs(info - (bits - 1)) < 1e-12,
+            'numerical_entropy', 'cyclic-register capacity saturation')
+    saturation.append({'hidden_bits': bits - 1, 'whole_future_cmi_bits': info})
+    if bits == 3:
+        # A one-step prefix need not encode the entire future.
+        require(any(a[0] == b[0] and a != b for a in whole for b in whole),
+                'exact_countercontrol', 'one-step prefix can lose whole-future distinctions')
+
+print(json.dumps({'status': 'pass', 'checks': sum(counts.values()),
+                  'check_kinds': counts,
+                  'permutations': 24, 'initial_laws': 3,
+                  'saturation': saturation}, indent=2))
diff --git a/verification/lean-manuscript-census.json b/verification/lean-manuscript-census.json
index c310e95db..8a11a8638 100644
--- a/verification/lean-manuscript-census.json
+++ b/verification/lean-manuscript-census.json
@@ -1556,6 +1556,15 @@
       "manuscript": [],
       "note": "Research candidate: constructs time-t joint law by pushing an arbitrary initial law through actual permutation iterates; transports memory and C3 bounds and bounds a genuine supremum over all natural time/horizon pairs. No publication-facing promotion or K3 change is made before successful CI and independent proof review. No posterior opacity, physical record mechanism or accumulation-without-reuse claim."
     },
+    {
+      "name": "entire visible future as an exact finite-image trajectory random variable",
+      "modules": [
+        "FullFutureMemory"
+      ],
+      "status": "kernel-only",
+      "manuscript": [],
+      "note": "Research companion: uses the finite image of the actual entire future sequence, proves pointwise orbit decoding and exact equality criterion, and applies discrete Shannon CMI on that finite image. Proves whole-trace capacity and a genuine supremum over all natural times. No infinite-product measure/limit equivalence, physical preparation or publication promotion is claimed before independent review and CI."
+    },
     {
       "name": "conditional k-token cone theorem: products, cone closure, the k-fold maxCone bound and CNOT plus rotation/cyclic invariance give the PSD cone of the k-fold Pauli dictionary (round KTOKEN-MAXCONE-1, reconstruction)",
       "modules": [
diff --git a/verification/lean-mathlib/OIBridge.lean b/verification/lean-mathlib/OIBridge.lean
index e1f222645..85e286cd8 100644
--- a/verification/lean-mathlib/OIBridge.lean
+++ b/verification/lean-mathlib/OIBridge.lean
@@ -19,6 +19,7 @@
 -/
 import OIBridge.Averaging
 import OIBridge.TrajectoryMemory
+import OIBridge.FullFutureMemory
 import OIBridge.ChiralCenterRecovery
 import Mathlib.RepresentationTheory.Invariants
 import Mathlib.RepresentationTheory.Character
diff --git a/verification/lean-mathlib/OIBridge/FullFutureMemory.lean b/verification/lean-mathlib/OIBridge/FullFutureMemory.lean
new file mode 100644
index 000000000..bfca0488f
--- /dev/null
+++ b/verification/lean-mathlib/OIBridge/FullFutureMemory.lean
@@ -0,0 +1,131 @@
+/-
+# The entire visible future as an exact finite-image random variable
+
+The codomain below is the image of the actual infinite sequence map on the finite
+state space, not a fixed finite prefix or a freely chosen predictive surrogate.
+Conditional information uses ordinary discrete Shannon entropy on this finite
+image. No infinite-product measure or limit theorem is invoked or certified.
+-/
+import OIBridge.TrajectoryMemory
+import Mathlib.Data.Fintype.OfMap
+
+namespace OIBridge.FullFutureMemory
+open OIBridge.FiniteEntropy OIBridge.HiddenMemory
+
+variable {V H : Type*} [Fintype V] [Fintype H]
+variable [DecidableEq V] [DecidableEq H]
+
+/-- The complete visible sequence strictly after the state supplied as input. -/
+def trace (step : V × H ≃ V × H) (q : V × H) : ℕ → V :=
+  fun j => (step^[j + 1] q).1
+
+/-- Actual whole-future sequences, with equal sequences identified exactly. -/
+def FutureTrace (step : V × H ≃ V × H) := Set.range (trace step)
+
+def encodeFuture (step : V × H ≃ V × H) (q : V × H) : FutureTrace step :=
+  ⟨trace step q, q, rfl⟩
+
+theorem encodeFuture_surjective (step : V × H ≃ V × H) :
+    Function.Surjective (encodeFuture step) := by
+  rintro ⟨f, ⟨q, rfl⟩⟩
+  exact ⟨q, rfl⟩
+
+/-- Finiteness comes from the finite source, despite the sequence-valued ambient type. -/
+instance finiteFutureTrace (step : V × H ≃ V × H) : Finite (FutureTrace step) := by
+  classical
+  letI : Fintype (FutureTrace step) :=
+    Fintype.ofSurjective (encodeFuture step) (encodeFuture_surjective step)
+  infer_instance
+
+noncomputable def futureTraceFintype (step : V × H ≃ V × H) :
+    Fintype (FutureTrace step) := Fintype.ofFinite _
+
+noncomputable def futureTraceDecidableEq (step : V × H ≃ V × H) :
+    DecidableEq (FutureTrace step) := Classical.decEq _
+
+attribute [local instance] futureTraceFintype futureTraceDecidableEq
+
+/-- The code identifies exactly equal entire futures; it retains every future coordinate. -/
+theorem encodeFuture_eq_iff (step : V × H ≃ V × H) (q q' : V × H) :
+    encodeFuture step q = encodeFuture step q' ↔
+      ∀ j : ℕ, (step^[j + 1] q).1 = (step^[j + 1] q').1 := by
+  constructor
+  · intro h j
+    exact congrArg (fun f : FutureTrace step => f.val j) h
+  · intro h
+    apply Subtype.ext
+    funext j
+    exact h j
+
+def futureRV (step : V × H ≃ V × H) (t : ℕ) (q : V × H) : FutureTrace step :=
+  encodeFuture step (step^[t] q)
+
+/-- Decoding any coordinate gives the original orbit's actual future observation. -/
+theorem futureRV_apply (step : V × H ≃ V × H) (t j : ℕ) (q : V × H) :
+    (futureRV step t q).val j = TrajectoryMemory.now step (t + (j + 1)) q := by
+  change (step^[j + 1] (step^[t] q)).1 = (step^[t + (j + 1)] q).1
+  rw [Nat.add_comm t (j + 1)]
+  exact congrArg Prod.fst
+    (Function.iterate_add_apply (step : V × H → V × H) (j + 1) t q).symm
+
+theorem finite_block_is_truncation (step : V × H ≃ V × H) (t L : ℕ) (q : V × H) :
+    (fun j : Fin L => (futureRV step t q).val j.val) =
+      TrajectoryMemory.future step t L q := rfl
+
+/-- The actual whole future obeys the same hidden-information bound, with no horizon parameter. -/
+theorem full_future_via_hidden [Nonempty H] (step : V × H ≃ V × H)
+    (μ : FiniteEntropy.Dist (V × H)) (t : ℕ) :
+    cmiBits μ.p (TrajectoryMemory.past step t) (TrajectoryMemory.now step t)
+        (futureRV step t) ≤
+      cmiBits μ.p (TrajectoryMemory.past step t) (TrajectoryMemory.now step t)
+        (TrajectoryMemory.hidden step t) ∧
+    cmiBits μ.p (TrajectoryMemory.past step t) (TrajectoryMemory.now step t)
+        (TrajectoryMemory.hidden step t) ≤ Real.logb 2 (Fintype.card H) := by
+  have h := capacity_floor_of_fun (TrajectoryMemory.realization step μ t) (encodeFuture step)
+  change cmiBits (marg μ.p (TrajectoryMemory.slice step t)) varHist varNow
+      (fun s => encodeFuture step (varNow s, varHid s)) ≤
+      cmiBits (marg μ.p (TrajectoryMemory.slice step t)) varHist varNow varHid ∧
+    cmiBits (marg μ.p (TrajectoryMemory.slice step t)) varHist varNow varHid ≤ _ at h
+  simp only [TrajectoryMemory.cmiBits_marg] at h
+  exact h
+
+theorem full_future_c3 [Nonempty H] (step : V × H ≃ V × H)
+    (μ : FiniteEntropy.Dist (V × H)) (t : ℕ) :
+    cmiBits μ.p (TrajectoryMemory.past step t) (TrajectoryMemory.now step t)
+      (futureRV step t) ≤ Real.logb 2 (Fintype.card H) :=
+  (full_future_via_hidden step μ t).1.trans (full_future_via_hidden step μ t).2
+
+/-- Genuine supremum over all natural times of the whole-trace conditional information. -/
+noncomputable def fullFutureIstar (step : V × H ≃ V × H)
+    (μ : FiniteEntropy.Dist (V × H)) : ℝ :=
+  sSup (Set.range fun t : ℕ =>
+    cmiBits μ.p (TrajectoryMemory.past step t) (TrajectoryMemory.now step t) (futureRV step t))
+
+theorem fullFutureIstar_le [Nonempty H] (step : V × H ≃ V × H)
+    (μ : FiniteEntropy.Dist (V × H)) : fullFutureIstar step μ ≤
+      Real.logb 2 (Fintype.card H) := by
+  apply csSup_le
+  · exact ⟨_, ⟨0, rfl⟩⟩
+  · rintro _ ⟨t, rfl⟩
+    exact full_future_c3 step μ t
+
+theorem full_future_capacity [Nonempty H] (step : V × H ≃ V × H)
+    (μ : FiniteEntropy.Dist (V × H)) :
+    (2 : ℝ) ^ fullFutureIstar step μ ≤ (Fintype.card H : ℝ) := by
+  have hc : (0 : ℝ) < (Fintype.card H : ℝ) := by
+    exact_mod_cast Fintype.card_pos_iff.2 ‹Nonempty H›
+  have hpow : (2 : ℝ) ^ fullFutureIstar step μ ≤
+      (2 : ℝ) ^ Real.logb 2 (Fintype.card H) :=
+    (Real.rpow_le_rpow_left_iff (by norm_num : (1 : ℝ) < 2)).2
+      (fullFutureIstar_le step μ)
+  rwa [Real.rpow_logb (by norm_num) (by norm_num) hc] at hpow
+
+#print axioms encodeFuture_surjective
+#print axioms encodeFuture_eq_iff
+#print axioms futureRV_apply
+#print axioms finite_block_is_truncation
+#print axioms full_future_via_hidden
+#print axioms full_future_c3
+#print axioms fullFutureIstar_le
+#print axioms full_future_capacity
+end OIBridge.FullFutureMemory