Information Loss under a Finite Free Group Quotient

Abstract

A finite free group quotient loses exactly the conditional information in its residual coordinate.

Theorem 1.1 (Finite free group quotient information loss).

$$\begin{array}{c}\forall G,Y,\mathrm{FiniteGroup}\left(G\right)\wedge \mathrm{Finite}\left(Y\right)\wedge \mathrm{FreeAction}\left(G,Y\right),\\ B=Y/G,s:B\to Y,\mathrm{section}\left(s\right),\\ Z,P,Q:\mathrm{PMF}\left(Y\right)\Rightarrow \\ H\left(Z\right)=H\left(Z_B\right)+\mathrm{Hcond}\left(Z_s\right)\wedge \\ H\left(Z\right)-H\left(Z_B\right)=\mathrm{Hcond}\left(Z_s\right)\wedge \\ (H\left(Z\right)-H\left(Z_B\right)=\log (\mathrm{card}\left(G\right))\Rightarrow \forall b,Z_B(b)\ne 0\Rightarrow Z_{\Gamma |b}=\mathrm{Unif}\left(G\right))\wedge \\ D(P\Vert Q)=D(P_B\Vert Q_B)+\sum _b{P}_B(b)\cdot D(P_{\Gamma |b}\Vert Q_{\Gamma |b})\wedge \\ (D(P_B\Vert Q_B)\ne \infty \Rightarrow D(P\Vert Q)-D(P_B\Vert Q_B)=\sum _b{P}_B(b)\cdot D(P_{\Gamma |b}\Vert Q_{\Gamma |b})).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Fusion/GroupQuotientInformationLoss.group_quotient_information_loss (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let a finite group G act freely on a finite set Y. A chosen section s of the genuine orbit quotient B = Y/G determines the equivalence c_s : Y equiv B x G used by the Lean declaration. For a PMF Z, write Z_B for its quotient pushforward and Z_s for its pushforward along c_s. Entropy is the repository finite Shannon entropy of the real mass underlying the PMF.

The first two conjuncts are respectively the Shannon chain rule in the quotient-residual coordinates and its information-loss rearrangement. The third is only an implication: attaining log(card G) forces every positive-mass conditional residual law of Z to be uniform. It does not assert the converse or constrain zero-mass fibers.

For arbitrary PMFs P and Q, the fourth conjunct is the unrestricted extended-nonnegative-real Kullback-Leibler chain rule. Its conditional divergences are weighted by the P quotient marginal. No positivity or absolute-continuity premise is added; infinite divergence is allowed.

The fifth conjunct names the quotient data-processing loss as total KL minus quotient KL and identifies it with the same weighted conditional divergence. Under the classical extended-value convention this subtraction identity is asserted when the quotient KL is finite, so the undefined infinity-minus-infinity case is not silently collapsed.

References

• Truth anchor: D5/S3/Entropy/Fusion/GroupQuotientInformationLoss.group_quotient_information_loss
• Dependency: D5/S3/Entropy/EntropyEquality
• Dependency: D5/S3/Entropy/Forgetting/DeterministicEntropyEquality