Commitment Information Upper Bound

Abstract

Conditional commitment information is bounded by commitment entropy given environment.

Theorem 1.1 (The commitment channel is bounded by conditional commitment entropy).

$$\begin{array}{c}\forall X:Type,E:Type,C:Type,B:Type,\\ [\mathrm{Fintype}(X)],[\mathrm{Fintype}(E)],[\mathrm{Fintype}(C)],[\mathrm{Fintype}(B)],\\ \mu :X\to \mathbb{R},e:X\to E,\\ c:X\to C,b:X\to B,\\ ((\forall x\in X,0\le \mu (x))\wedge \sum _{x\in X}\mu (x)=1)\Rightarrow \\ \mathrm{conditionalMutualInformation}(\mathrm{pushforward}(x\mapsto (e(x),(c(x),b(x))),\mu ))\le \mathrm{targetResidualEntropy}(\mu ,e,c).\end{array}$$

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

Source. Repository-derived.

Commentary.

A normalized nonnegative mass on a finite sample carrier constructs the environment, current commitment, and future behavior through their canonical joint pushforward law.

Enriching the future record with the commitment makes recovery exact, so the frozen saturation theorem identifies its information with the commitment entropy remaining after the environment readout.

Forgetting the added commitment coordinate recovers the actual future record. The frozen deterministic-forgetting theorem then gives the displayed upper bound.

References

• Truth anchor: D5/S3/Entropy/Forgetting/CommitmentInformationUpperBound.commitment_information_le_residual_entropy
• Dependency: D5/S3/Entropy/ConditionalEntropyEquality
• Dependency: D5/S3/Entropy/Forgetting/CommitmentInformationSaturation