Joint Prediction Product Fullness
Abstract
Joint prediction fills the product exactly when every pair of prediction fibers meets.
Theorem 1.1 (Joint prediction product fullness criterion).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Fusion/JointPredictionProductFullness.joint_prediction_product_fullness_criterion (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let a finite realized state type map surjectively onto a fused state type, and let an injective joint prediction map send each fused state to its two component predictions. The joint map is surjective exactly when every pair of component prediction fibers has a common realizing state.
For finite state spaces, injectivity turns product fullness into an exact cardinality test: the fused state count equals the product of the component state counts. Pinned Mathlib supplies the exact cardinality bridge Nat.bijective_iff_injective_and_card and the product identity Nat.card_prod. Direct local source search found these declarations; local smart-search returned no declarations, Loogle returned zero shaped matches, and LeanSearch’s API endpoint returned HTTP 404.
The theorem proves compatibility fullness for two finite prediction coordinates. It does not assert probabilistic independence, an entropy identity, or a decomposition for more than two factors.
References
- Truth anchor:
D5/S3/ObserverMemory/Fusion/JointPredictionProductFullness.joint_prediction_product_fullness_criterion