Common Prediction Factor

Abstract

The dynamics-stable common prediction quotient has a unique surjective factor.

Theorem 1.1 (The common prediction factor has the universal property).

$$\begin{array}{c}\forall Y,O_1,O_2,W,\\ u:Y\to Y,v:W\to W,\\ q_1:Y\to O_1,q_2:Y\to O_2,\\ r:Y\to W,\mathrm{Surjective}\left(r\right),\\ r\circ u=v\circ r,\\ a_1:\mathrm{Quotient}(\mathrm{KerTr}\left(u,q_1\right))\to W,a_2:\mathrm{Quotient}(\mathrm{KerTr}\left(u,q_2\right))\to W,\\ r=a_1\circ {\pi }_{q_1},r=a_2\circ {\pi }_{q_2}\Rightarrow \\ \exists !h:\mathrm{Quotient}(\mathrm{StableJoin}\left(u,\mathrm{KerTr}\left(u,q_1\right),\mathrm{KerTr}\left(u,q_2\right)\right))\to W,\mathrm{Surjective}\left(h\right)\wedge \\ r=h\circ {\pi }_{common}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Fusion/CommonPredictionFactor.common_prediction_factor_universal_property (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let u update source states, and let q1 and q2 be readouts. Each readout determines the canonical complete-itinerary kernel. Their common relation is constructed as the least equivalence relation containing both kernels and preserved by u.

Suppose a surjection r onto W intertwines u with an update v on W. Also suppose r factors through each complete-itinerary quotient by maps a1 and a2. Then there is a unique surjective map h from the common quotient to W, and h factors the canonical projection.

The two given factorizations put both itinerary kernels inside the kernel of r, while the intertwining equation makes that kernel stable under u. The infimum construction therefore lies inside the kernel of r. Pinned Mathlib quotient lift, surjectivity, and uniqueness results then supply the asserted map directly.

References

• Truth anchor: D5/S3/ObserverMemory/Fusion/CommonPredictionFactor.common_prediction_factor_universal_property
• Dependency: D5/S3/ObserverMemory/Prediction/ItineraryCompletion