Belief Set Sufficiency

Abstract

Equal compatible belief sets determine equal future observation trajectories.

Theorem 1.1 (The compatible belief set is sufficient for future trajectories).

$$\begin{array}{c}\forall X,U,O:\mathrm{Type},\\ F:U\to \left(X\to X\right),q:X\to O,\\ o_1,o_2:O,h_1,h_2:\mathrm{List}(U\times O),\\ \mathrm{compatibleBelief}(F,q,o_1,h_1)=\mathrm{compatibleBelief}(F,q,o_2,h_2)\Rightarrow \\ \forall a:\mathrm{List}(U),\mathrm{possibleObservationTrajectories}(F,q,o_1,h_1,a)=\mathrm{possibleObservationTrajectories}(F,q,o_2,h_2,a).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/PredictionFactors/BeliefSetSufficiency.belief_set_sufficiency (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let X be the hidden-state type, U the action type, and O the observation type. The compatible belief set starts with every state having the initial observation, then processes each action-observation pair by applying the indexed update and retaining exactly the states with the reported next observation.

For a future action word, the observation trajectory of a state reads the canonical controlled behavior on every prefix of that word. Possible trajectories are constructed independently from hidden start and final states connected by every observed transition in the concrete history.

If two concrete histories generate the same compatible belief set, their possible trajectory sets are equal for every future action word. The statement retains both histories publicly. The proof first identifies the final states produced by the recursive belief update with those produced by the independent transition-path relation.

The module directly reuses the repository’s controlledBehavior semantics and pinned Mathlib’s exact List.inits prefix construction. Searches found no existing theorem combining them with recursively updated belief sets.

References

• Truth anchor: D5/S3/ObserverMemory/PredictionFactors/BeliefSetSufficiency.belief_set_sufficiency
• Dependency: D5/S3/ObserverMemory/Prediction/ControlledBehaviorUniversality