Deterministic Readout Entropy Decomposition

Abstract

A deterministic finite readout splits source entropy into retained and residual parts, while garbling can only increase the residual.

Theorem 1.1 (Finite deterministic readouts split entropy and order residuals).

$$\forall X\in Type,Fine\in Type,Coarse\in Type,mu\in X\to Real,q0\in \mathrm{Concept}\left(X,Fine\right),q1\in \mathrm{Concept}\left(X,Coarse\right),r\in Fine\to Coarse,\left(\left(\mathrm{Fintype}\left(X\right)\wedge \left(\mathrm{Fintype}\left(Fine\right)\wedge \mathrm{Fintype}\left(Coarse\right)\right)\right)\wedge \left(\left(\forall x\in X,0\le mu\left(x\right)\right)\wedge \left(\mathrm{sum}\left(mu\right)=1\wedge q1=\mathrm{compose}\left(r,q0\right)\right)\right)\right)\Rightarrow \left(\mathrm{shannonEntropy}\left(mu\right)=\mathrm{conceptInformation}\left(mu,q0\right)+\mathrm{conceptResidual}\left(mu,q0\right)\wedge \mathrm{conceptResidual}\left(mu,q0\right)\le \mathrm{conceptResidual}\left(mu,q1\right)\right)$$

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

Source. Repository-derived.

Commentary.

The source, fine-readout, and coarse-readout carriers are finite. The source mass is nonnegative and normalized, so it represents the finite random state in the theorem.

The first conjunct identifies source entropy with the sum of the classification entropy retained by the fine readout and the conditional entropy remaining in its fibers.

The equation coarse = forget composed with fine is the deterministic garbling premise. The second conjunct states that the fine readout leaves no more conditional entropy than the coarse one.

References

• Truth anchor: D5/S3/Entropy/Observation/DeterministicReadoutEntropyDecomposition.deterministic_readout_entropy_decomposition
• Dependency: D5/S3/ConceptDynamics/Information/RefinementEntropyMonotonicity
• Dependency: D5/S3/Entropy/Fusion/QuotientFiberDecomposition