11.1. 3. The extension by component split🔗

Units and conventions are those of section 0 of the contact page: entropies and mutual informations are in nats, conditional sums range over positive-probability conditioning events, and 0\ln0=0. A finite latent L of a law p, its budgets M_L=I(X;Y\mid L) and B_L=I(L;X\mid Y)+I(L;Y\mid X), the stochastic optimum \tau(p)=\inf_L(M_L+B_L), the score D_p(f) of a deterministic map f and the deterministic optimum T(p)=\min_fD_p(f) are as in (D3). All alphabets are finite and nonempty; X,Y and \mathcal X,\mathcal Y denote the same coordinate alphabets. Every law on this page is a law on the fixed rectangle \mathcal X\times\mathcal Y.

Write S=\{z:p(z)>0\}. This set is nonempty. Connectedness of the support, as a bipartite graph between the active rows and the active columns of S, is defined on the setup page, together with its Lean form stoch_to_det.IsConnected. On this page K is the component label, not the replica budget K of the replica page, and C is any nonnegative constant.

Extension by component split. Given some C\ge0 with T(q)\le C\tau(q) for every law q of connected

support, the same inequality holds for every finite law.

Splitting at the common component label preserves the two leakage terms and isolates one nonnegative entropy term in the mutual information. This gives an additive proof for every nonnegative coefficient, with no positivity assumption on the resulting value of \tau.

Lean: stoch_to_det.ComponentDecomp and stoch_to_det.exists_componentDecomp (NaturalLatents/Upstream/Connected.lean). A component decomposition of p is a finite family of weights forming a probability vector and of probability laws on \mathcal X\times\mathcal Y with connected supports whose mixture is p, such that support cells of two distinct parts share neither a row nor a column; its parts are the laws \bar p_k. The structure allows a zero weight, although the construction in exists_componentDecomp makes every weight positive, and the label K is the private function componentIndex.

Lean: there is no public statement of (E3.C). The private lemma restrict_score_gap (NaturalLatents/Upstream/Connected.lean) states, for every latent of p, that the weighted sum of the scores of its conditional latents on the parts equals its score minus H_p(K\mid L), written as the prior average of the entropies of the conditional laws of K given each label; the private lemma glueLatent_score states the case of a latent glued from latents of the parts, where H_p(K\mid L)=0. Both are in bits and are proved from the score identity stoch_to_det.Latent.score_eq (NaturalLatents/Upstream/Envelope.lean) and the split of the entropies of p over the parts (the private Psi_eq_components and Phi_fiber_decomp), not from the chain rule. On a part of weight zero the private restrictLatent uses the constant latent.

Lean: stoch_to_det.sum_components_tau_le and stoch_to_det.T_le_sum_components (NaturalLatents/Upstream/Connected.lean), in bits, for a component decomposition D of p:

theorem sum_components_tau_le {p : α × β → ℝ} (hp : IsPMF p) (D : ComponentDecomp p) :
    (∑ i, D.wt i * tau (D.part i)) ≤ tau p
theorem T_le_sum_components {p : α × β → ℝ} (hp : IsPMF p) (D : ComponentDecomp p) :
    T p ≤ ∑ i, D.wt i * T (D.part i)

The first restricts one attaining latent of p, given by stoch_to_det.exists_tau_optimal_latent (NaturalLatents/Upstream/Envelope.lean), rather than every latent, through the private restrict_score_le. In Lean T is an infimum over deterministic latents, and the second glues attaining deterministic latents of the parts, given by stoch_to_det.exists_T_optimal_latent, with the private glueLatent and glueLatent_isDet; the glued labels are pairs of a part and a label of that part.

Lean: NaturalLatents.General.extension_of_connected (NaturalLatents/General/Extension.lean), in bits, which is stoch_to_det.reduce_to_connected (NaturalLatents/Upstream/Connected.lean) applied to laws Law X Y:

theorem extension_of_connected (C : ℝ) (hC : 0 ≤ C)
    (hconnected : ∀ (q : Law X Y), stoch_to_det.IsPMF q →
      stoch_to_det.IsConnected (stoch_to_det.support q) →
      stoch_to_det.T q ≤ C * stoch_to_det.tau q)
    {p : Law X Y} (hp : stoch_to_det.IsPMF p) :
    stoch_to_det.T p ≤ C * stoch_to_det.tau p
theorem reduce_to_connected (C : ℝ) (hC : 0 ≤ C)
    (h : ∀ q : α × β → ℝ, IsPMF q → IsConnected (support q) → T q ≤ C * tau q) :
    ∀ q : α × β → ℝ, IsPMF q → T q ≤ C * tau q

reduce_to_connected proves the chain (E3.J) from T_le_sum_components and sum_components_tau_le, using hC in the last step exactly as the page does. NaturalLatents.T_le_c_mul_tau (NaturalLatents/Main.lean) applies extension_of_connected, after bits_of_nats (NaturalLatents/General/Nats.lean) converts the connected bound to bits, with C = c, the constant NaturalLatents.c := 13999 / 2000, and its nonnegativity c_nonneg.