Stable Window Conditional Entropy

Abstract

Stable finite observation kernels have zero next-readout conditional entropy, and a full-support law detects kernel stability.

Theorem 1.1 (Kernel stability and zero conditional entropy).

$$\begin{array}{c}\forall Y,O:\mathrm{FiniteType},\\ F:Y\to Y,q:Y\to O,n:N,\\ ((\mathrm{kernel}(\mathrm{futureReadoutWord}(F,q,n))=\mathrm{kernel}(\mathrm{futureReadoutWord}(F,q,n+1)))\Rightarrow \forall p:Y\to R,(\mathrm{ProbabilityLaw}(p))\Rightarrow (\mathrm{conditionalEntropy}(\mathrm{nextReadoutJointLaw}(F,q,p,n))=0))\wedge \\ (\forall p:Y\to R,(\mathrm{ProbabilityLaw}(p)\wedge \mathrm{FullSupport}(p))\Rightarrow (\mathrm{conditionalEntropy}(\mathrm{nextReadoutJointLaw}(F,q,p,n))=0)\Rightarrow (\mathrm{kernel}(\mathrm{futureReadoutWord}(F,q,n))=\mathrm{kernel}(\mathrm{futureReadoutWord}(F,q,n+1)))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Observation/StableWindowConditionalEntropy.stable_window_conditional_entropy (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite word and its consecutive kernels are the canonical futureReadoutWord objects. The joint law is the deterministic pushforward pairing the word through depth n with the next readout.

If the consecutive kernels agree, the next readout is constant on every word fiber. The imported point-mass criterion therefore makes its conditional entropy zero for every normalized initial law, including laws that do not have full support.

Conversely, strict positivity gives every state and every realized word positive mass. Zero conditional entropy then forces both next readouts in any common word fiber to equal the same point-mass value, which reconstructs equality of the consecutive kernels.

References

• Truth anchor: D5/S3/Entropy/Observation/StableWindowConditionalEntropy.stable_window_conditional_entropy
• Dependency: D5/S3/ObserverMemory/Prediction/ConditionalEntropyStability