Deterministic Entropy Step

Abstract

A deterministic finite-state step loses conditional entropy, with equality exactly at support recovery.

Theorem 1.1 (Deterministic steps lose conditional entropy).

$\forall t, H t - H t 1 = Ct \land Ct \geq 0 \land (H t - H t 1 = 0 ⟺ I nj ec t i v e O n S u pp or t) .$

Proof. Machine-checked in Lean as D5/S3/Entropy/Forgetting/DeterministicEntropyStep.deterministic_entropy_step (✓ std3). ∎

Source. Repository-derived.

Commentary.

The trajectory law is generated by repeated deterministic pushforward from the initial probability law.

The graph-supported transition joint supplies the conditional entropy; the support qualifier excludes zero-mass states from recovery.

Truth anchor: D5/S3/Entropy/Forgetting/DeterministicEntropyStep.deterministic_entropy_step
Dependency: D5/S3/Entropy/EntropyNonneg
Dependency: D5/S3/Entropy/Forgetting/DeterministicEntropyEquality
Dependency: D5/S3/Entropy/Forgetting/TrajectoryEntropyTelescoping