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 (The first marginal of a joint pushforward).

$$\forall X:\mathrm{Type},\forall A:\mathrm{Type},\forall B:\mathrm{Type},[\mathrm{Fintype}\left(X\right)][\mathrm{Fintype}\left(B\right)]\forall mu:X\to \mathbb{R},\forall f:X\to A,\forall g:X\to B,\mathrm{marginal}\left(\mathrm{pushforward}\left(x\mapsto (f(x),g(x)),mu\right)\right)=\mathrm{pushforward}\left(f,mu\right)$$

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

Source. Repository-derived.

Commentary.

Summing the joint law of two readouts over the second coordinate gives the law of the first readout. The coordinate marginal identity uses this equality, and the product contextuality construction applies it to finite restriction fibers.

Theorem 1.2 (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.marginal_pushforward_pair
• 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