Canonical Predictive-State Sufficiency

Abstract

The canonical conditional-future-law state makes the complete past and future conditionally independent.

Theorem 1.1 (The predictive state retains every past influence on the future).

$$\begin{array}{c}\forall Past,Future:\mathrm{Type},[\mathrm{Fintype}(Past)],[\mathrm{Fintype}(Future)],\\ \pi :\mathrm{PMF}(Past),K:Past\to \mathrm{PMF}(Future),\\ S:=\mathrm{range}(K),\epsilon :Past\to S:=\mathrm{rangeFactorization}(K),\\ J:\mathrm{Product}(Past,\mathrm{Product}(S,Future))\to \mathbb{R}:=\lambda \mathrm{Triple}(h,s,f),\mathrm{ite}(\epsilon (h)=s,\mathrm{toReal}(\pi (h))\cdot \mathrm{toReal}(K(h)(f)),0),\\ \forall h:Past,s:S,f:Future,\\ J(\mathrm{Triple}(h,s,f))\cdot \mathrm{marginal}(\mathrm{yFirstLaw}(J),s)=\mathrm{xyProjection}(J,\mathrm{Pair}(h,s))\cdot \mathrm{xzProjection}(\mathrm{yFirstLaw}(J),\mathrm{Pair}(s,f)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/PredictionFactors/CanonicalPredictiveStateSufficiency.canonical_predictive_state_is_sufficient (✓ std3). ∎

Source. Repository-derived.

Commentary.

Past and Future are finite alphabets. The process is constructed from a past prior and its conditional future PMF channel.

The map epsilon is the canonical range factorization of the complete conditional future law, matching the repository’s causal-state carrier. The displayed cross-product equality is the finite joint-law criterion for conditional independence of past and future given S.

The proof identifies the induced law with a channel-generated Markov law and applies the frozen Markov channel theorem. No positive-support condition on the past prior is required.

References

• Truth anchor: D5/S3/ObserverMemory/PredictionFactors/CanonicalPredictiveStateSufficiency.canonical_predictive_state_is_sufficient
• Dependency: D5/S3/Entropy/Submodularity/MarkovDataProcessing