Multi-Target Information Chain

Abstract

The total finite information cost of adjoining a heterogeneous target family is independent of its order and is the sum of ordered conditional contributions.

Theorem 1.1 (Total target information is independent of target order).

$$\begin{array}{c}\forall n:\mathbb{N},X,B:\mathrm{Type},\\ Y:\mathrm{Fin}\left(n\right)\to \mathrm{Type},\\ (\mathrm{Fintype}\left(X\right)\wedge \mathrm{Fintype}\left(B\right)\wedge \forall i:\mathrm{Fin}\left(n\right),\mathrm{Fintype}\left(Y(i)\right))\Rightarrow \\ \forall mu:\mathrm{PMF}\left(X\right),C:X\to B,\\ T:\forall i:\mathrm{Fin}\left(n\right),X\to Y(i),\\ pi:\mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),\\ \mathrm{let}{p}_0:=\mathrm{orderedCompletionLaw}\left(mu,C,T,\mathrm{refl}\left(\mathrm{Fin}\left(n\right)\right)\right),\\ p_{pi}:=\mathrm{orderedCompletionLaw}\left(mu,C,T,pi\right)\\ \mathrm{in}H\left(p_0\right)-H\left(\mathrm{firstReadoutMarginal}\left(p_0\right)\right)=\sum _{k<n}\mathrm{prefixConditionalEntropy}\left(p_{pi},k\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

Each target value is tagged by its original finite index and placed after the concept readout in the repository’s recursive FutureWord carrier. A permutation changes only the target coordinates and fixes the initial concept coordinate.

The frozen finite-word chain rule expands the permuted law into one full-prefix conditional entropy for each target. Entropy invariance under the induced coordinate equivalence identifies its total cost with the canonical target order.

The PMF binder supplies the finite probability model. No common target codomain is assumed: the family Y may vary with the target index.

References

• Truth anchor: D5/S3/Entropy/Observation/MultiTargetInformationChain.multi_target_information_chain
• Dependency: D5/S3/Entropy/Forgetting/CapacityMonotone
• Dependency: D5/S3/Entropy/NamingWindow/FutureWordInformationChain
• Dependency: D5/S3/Entropy/Relabeling/InjectiveInvariance