Independent Prediction State Cardinality

Abstract

Independent predictive components have a product completion and multiplicative finite state count.

Theorem 1.1 (Independent prediction state cardinality is multiplicative).

$$\begin{array}{c}\forall tau1,tau2,q1,q2,\\ [\mathrm{Finite}\mathrm{CompletedState}\left(tau1,q1\right)][\mathrm{Finite}\mathrm{CompletedState}\left(tau2,q2\right)],\\ \mathrm{Nonempty}(\mathrm{CompletedState}\left(\mathrm{productUpdate}\left(tau1,tau2\right),\mathrm{productReadout}\left(q1,q2\right)\right)\equiv (\mathrm{CompletedState}\left(tau1,q1\right))\times (\mathrm{CompletedState}\left(tau2,q2\right)))\wedge \\ \mathrm{predictiveStateCount}\left(\mathrm{CompletedState}\left(\mathrm{productUpdate}\left(tau1,tau2\right),\mathrm{productReadout}\left(q1,q2\right)\right)\right)=\mathrm{predictiveStateCount}\left(\mathrm{CompletedState}\left(tau1,q1\right)\right)\times \mathrm{predictiveStateCount}\left(\mathrm{CompletedState}\left(tau2,q2\right)\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

The predictive state count is the finite cardinality of a completed-state carrier. Assume that the completed states of both component systems are finite.

For the componentwise product update and paired product readout, the global completed-state quotient is equivalent to the Cartesian product of the two component quotients. Consequently its predictive state count is the product, rather than the sum, of the two component counts.

The previously established independent-product equivalence supplies the decomposition. Invariance of finite cardinality under equivalence and the cardinality rule for product types then give the multiplication law. The result concerns two components and does not assert a general finite-family decomposition.

References

• Truth anchor: D5/S3/ObserverMemory/Fusion/IndependentPredictionStateCardinality.finite_independent_prediction_state_cardinality
• Dependency: D5/S3/ObserverMemory/Fusion/IndependentProductCompletion