Predictive Sufficiency Descent

Abstract

Predictive completion carries the update and the current readout.

Theorem 1.1 (The update and readout descend to predictive completion).

$$\begin{gathered} \forall X,O:\mathrm{Type},F:X\to X,q:X\to O, \\ (\forall x,\mathrm{completionUpdate}\left(F,q\right)(\mathrm{completionProjection}\left(F,q\right)(x))=\mathrm{completionProjection}\left(F,q\right)(F(x)))\wedge \\ (\forall x,\mathrm{completionReadout}\left(F,q\right)(\mathrm{completionProjection}\left(F,q\right)(x))=q(x)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Sufficiency/PredictiveSufficiencyDescent.predictive_sufficiency_descent (✓ std3). ∎

Source. Repository-derived.

Commentary.

The completion carrier is the canonical quotient by equality of complete future readout itineraries. Its projection, update, and readout are the existing family primitives.

The first public equation gives the induced update on every quotient class. The second gives the descended current readout on the same canonical class; neither object is reconstructed in this module.

References

• Truth anchor: D5/S3/ConceptDynamics/Sufficiency/PredictiveSufficiencyDescent.predictive_sufficiency_descent
• Dependency: D5/S3/ObserverMemory/Refinement/PredictionCompletion