Equality in the Green-Class Window Entropy Bound

Abstract

A naming window reaches its entropy bound exactly when every pinned coordinate law is uniform on the full alphabet.

Theorem 1.1 (Maximum window entropy characterizes uniform coordinates).

$$\begin{array}{c}H(\mathrm{windowLaw}(\mathrm{coordLaw}(mu)))=n\times \mathrm{namingDim}(O)\times \log 2\iff \\ \forall i\in S,\mathrm{coordLaw}(mu,i)=(a\mapsto \mathrm{card}(O{)}^{-1}).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/NamingWindow/GreenClassWindowEntropyEquality.shannonEntropy_windowLaw_eq_namingDim_iff_uniform (✓ std3). ∎

Source. Repository-derived.

Commentary.

GreenClassWindowEntropy reduces the entropy of a finite naming window to the sum of its coordinate entropies and bounds each summand by log(card O). Equality of the finite sums forces every coordinate summand to attain that same upper bound.

EntropyEquality then identifies each maximizing coordinate law with the uniform law on all of O. Conversely, uniformity at every coordinate makes every summand maximal, so additivity gives equality for the window.

Only coordinates in S are constrained. When S is empty, both the entropy identity and the coordinatewise condition are vacuous, so the equivalence still holds without a separate exception.

References

• Truth anchor: D5/S3/Entropy/NamingWindow/GreenClassWindowEntropyEquality.shannonEntropy_windowLaw_eq_namingDim_iff_uniform
• Dependency: D5/S3/Entropy/EntropyEquality
• Dependency: D5/S3/Entropy/NamingWindow/GreenClassWindowEntropy