Predictive Completion as a Maximal Invariant Quotient

Abstract

The maximal invariant future kernel carries the canonical predictive quotient.

Theorem 1.1 (The complete-future kernel yields the coarsest predictive refinement).

$$\begin{array}{c}\forall Y,O:\mathrm{Type},\\ tau:Y\to Y,q:Y\to O,\\ \mathrm{let}Kinf:=\ker \left(\mathrm{completeItinerary}\left(tau,q\right)\right),\\ piInf:=\mathrm{completionProjection}\left(tau,q\right),\\ Kpi:=\ker \left(piInf\right)\\ \mathrm{in}[Kpi=Kinf\wedge \\ Kinf=\mathrm{gfp}\left(\mathrm{refinementOperator}\left(tau,q\right)\right)\wedge \\ Kinf\subseteq \mathrm{observationKernel}\left(q\right)\wedge \\ (\forall p:Y\times Y,p\in Kinf\Rightarrow (tau\left(\mathrm{fst}\left(p\right)\right),tau\left(\mathrm{snd}\left(p\right)\right))\in Kinf)\wedge \\ (\forall R:\mathrm{Set}\left(Y\times Y\right),R\subseteq \mathrm{observationKernel}\left(q\right)\Rightarrow (\forall p:Y\times Y,p\in R\Rightarrow (tau\left(\mathrm{fst}\left(p\right)\right),tau\left(\mathrm{snd}\left(p\right)\right))\in R)\Rightarrow R\subseteq Kinf)\wedge \\ (\exists !readoutBar:\mathrm{CompletedState}\left(tau,q\right)\to O,q=readoutBar\circ piInf)\wedge \\ \exists !updateBar:\mathrm{CompletedState}\left(tau,q\right)\to \mathrm{CompletedState}\left(tau,q\right),piInf\circ tau=updateBar\circ piInf].\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/RefinementClosure/PredictiveCompletionMaximalInvariantQuotient.predictive_completion_maximal_invariant_quotient (✓ std3). ∎

Source. Repository-derived.

Commentary.

The completed kernel is the equality kernel of the canonical complete itinerary. The projection is the canonical map to its kernel quotient, and the statement explicitly identifies the projection kernel with the completed kernel.

The completed kernel is the greatest fixed point of one-step refinement. It lies inside the current readout kernel, is forward invariant, and contains every relation satisfying those two conditions.

The quotient itself is public: both the current readout and source update descend uniquely through its surjective canonical projection. The proof applies the frozen greatest-fixed-point theorem and pinned quotient exactness and surjectivity rules.

References

• Truth anchor: D5/S3/ObserverMemory/RefinementClosure/PredictiveCompletionMaximalInvariantQuotient.predictive_completion_maximal_invariant_quotient
• Dependency: D5/S3/ObserverMemory/Refinement/PredictionCompletion
• Dependency: D5/S3/ObserverMemory/RefinementClosure/CompletionKernelGreatestFixedPoint