Predictive-State Unifilar Update

Abstract

Complete future laws induce an almost-sure single-valued predictive-state update.

Theorem 1.1 (The complete-future-law quotient has a unifilar update).

$$\forall History\in Type,Symbol\in Type,K\in History\to \mathrm{ProbabilityMeasure}\left(Nat\to Symbol\right),extend\in History\to \left(Symbol\to History\right),\left(\left(\mathrm{MeasurableSpace}\left(Symbol\right)\wedge \left(\mathrm{MeasurableSingletonClass}\left(Symbol\right)\wedge \mathrm{Countable}\left(Symbol\right)\right)\right)\wedge \left(\forall h\in History,a\in Symbol,0<\mathrm{toMeasure}\left(K\left(h\right)\right)\left(\mathrm{setOf}\left(\Lambda x,x\left(0\right)=a\right)\right)\Rightarrow \mathrm{toMeasure}\left(K\left(extend\left(h,a\right)\right)\right)=\mathrm{scale}\left(\mathrm{inverse}\left(\mathrm{toMeasure}\left(K\left(h\right)\right)\left(\mathrm{setOf}\left(\Lambda x,x\left(0\right)=a\right)\right)\right),\mathrm{map}\left(\Lambda xn,x\left(n+1\right),\mathrm{restrict}\left(\mathrm{toMeasure}\left(K\left(h\right)\right),\mathrm{setOf}\left(\Lambda x,x\left(0\right)=a\right)\right)\right)\right)\right)\right)\Rightarrow \left(\exists T\in \mathrm{Quotient}\left(\ker \left(K\right)\right)\to \left(Symbol\to \mathrm{Quotient}\left(\ker \left(K\right)\right)\right),\left(\forall h\in History,a\in Symbol,0<\mathrm{toMeasure}\left(K\left(h\right)\right)\left(\mathrm{setOf}\left(\Lambda x,x\left(0\right)=a\right)\right)\Rightarrow T\left(\mathrm{quotientClass}\left(K,h\right),a\right)=\mathrm{quotientClass}\left(K,extend\left(h,a\right)\right)\right)\wedge \left(\forall h\in History,\mathrm{AlmostEverywhere}\left(\mathrm{map}\left(\Lambda x,x\left(0\right),\mathrm{toMeasure}\left(K\left(h\right)\right)\right),\Lambda a,T\left(\mathrm{quotientClass}\left(K,h\right),a\right)=\mathrm{quotientClass}\left(K,extend\left(h,a\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/ContextUpdates/PredictiveStateUnifilarUpdate.unifilar_predictive_update (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each history is assigned a probability measure on infinite symbol streams. Histories with the same full measure define one predictive state.

For a positive first-symbol cylinder, extending the history is required to realize the normalized restriction to that cylinder, pushed forward by the tail map. This is the public process consistency premise.

The constructed quotient update sends every positive symbol to the class of the extended history. Countability of the symbol carrier then turns that pointwise rule into the displayed almost-everywhere next-symbol statement.

References

• Truth anchor: D5/S3/ObserverMemory/ContextUpdates/PredictiveStateUnifilarUpdate.unifilar_predictive_update