Predictive Completion under Observation Refinement

Abstract

Observation refinement induces a unique surjective map of predictive completions.

Definition 1.1 (Completed states quotient equality of complete itineraries).

$$\forall Y\in \mathrm{Type},O\in \mathrm{Type},update\in Y\to Y,readout\in Y\to O,\mathrm{CompletedState}(update,readout)=\mathrm{Quotient}(\ker (\mathrm{completeItinerary}(update,readout)))$$

Formalization. D5/S3/ObserverMemory/Refinement/PredictionCompletion.CompletedState (✓ std3).

Source. Repository-derived.

Commentary.

For an update and readout on Y, the completed state is the quotient of Y by the kernel setoid of the complete future-itinerary map.

Definition 1.2 (The current readout descends to predictive completion).

$$\forall Y\in \mathrm{Type},O\in \mathrm{Type},update\in Y\to Y,readout\in Y\to O,\mathrm{completionReadout}(update,readout):\mathrm{CompletedState}(update,readout)\to O,\mathrm{completionReadout}(update,readout)=\mathrm{QuotientLift}(readout,\mathrm{timeZeroWellDefined}(update,readout))$$

Formalization. D5/S3/ObserverMemory/Refinement/PredictionCompletion.completionReadout (✓ std3).

Source. Repository-derived.

Commentary.

The current readout on a completed state is the quotient lift of the original readout. Equality of complete itineraries implies equality at time zero, which supplies the lift’s well-definedness proof.

Theorem 1.3 (Refinement induces the canonical predictive quotient map).

$$\forall Y\in \mathrm{Type},O\in \mathrm{Type},P\in \mathrm{Type},update\in Y\to Y,fine\in Y\to O,coarse\in Y\to P,forget\in O\to P,hfactor\in coarse=forget\circ fine,\ker (\mathrm{completeItinerary}(update,fine))\subseteq \ker (\mathrm{completeItinerary}(update,coarse))\wedge \exists !descend:\mathrm{Function}(\mathrm{CompletedState}(update,fine),\mathrm{CompletedState}(update,coarse)),\mathrm{Surjective}(descend)\wedge \left(\mathrm{completionProjection}(update,coarse)=descend\circ \mathrm{completionProjection}(update,fine)\wedge \left(descend\circ \mathrm{completionUpdate}(update,fine)=\mathrm{completionUpdate}(update,coarse)\circ descend\wedge \mathrm{completionReadout}(update,coarse)\circ descend=forget\circ \mathrm{completionReadout}(update,fine)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Refinement/PredictionCompletion.observation_refinement_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Suppose the coarse readout is obtained by applying forget to the fine readout. Applying forget at every time sends equality of complete fine itineraries to equality of complete coarse itineraries.

The repository theorem relative_identity_refinement then gives the unique surjection between the two kernel quotients and its projection factorization. Quotient induction verifies that the same map intertwines the induced update and current readout.

Pinned Mathlib supplies Setoid.map_of_le, Setoid.lift_unique, Quotient.map, and Quotient.lift through the imported repository modules. Loogle and third-party searches found no declaration combining the relation, uniqueness, surjectivity, and both intertwining equations.

References

• Truth anchor: D5/S3/ObserverMemory/Refinement/PredictionCompletion.CompletedState
• Truth anchor: D5/S3/ObserverMemory/Refinement/PredictionCompletion.completionReadout
• Truth anchor: D5/S3/ObserverMemory/Refinement/PredictionCompletion.observation_refinement_completion
• Dependency: D5/S0/Rewriting/Quotients/RelativeIdentityRefinement
• Dependency: D5/S3/ObserverMemory/Prediction/ItineraryCompletion