For a Fin M-valued encoder output Jn, a finite source block Xn, and any side-information block Yn, the mutual-information difference is bounded by the log-cardinality rate: (I(Jn; Xn) − I(Jn; Yn)).toReal ≤ log M.

Since I(Jn; Yn) ≥ 0, the truncated difference is ≤ I(Jn; Xn), and I(Jn; Xn).toReal = H(Jn) − H(Jn | Xn) ≤ H(Jn) ≤ log |Fin M| = log M (MaxEntropy.entropy_le_log_card + condEntropy_nonneg). This is the WZ analogue of the rate-distortion mutualInfo_block_le_log_card.

The source pmf fun p ↦ P_XY.real {p} of a probability measure lies in the standard simplex. @audit:ok

Markov chain Y − X − U on the factorizable manifold. For a factorizable joint q(x,y,u) = κ(u|x)·P_XY(x,y), realized as the discrete measure wzPmfMeasure q on α × β × V, the coordinates satisfy the Markov chain Y → X → U: U is appended to (X, Y) by the conditioner-only kernel κ, so U is conditionally independent of Y given X. This is the measure-form content that the data-processing inequality mutualInfo_le_of_markov consumes.

The U-given-X kernel Q x = κ(·|x) is built discretely; isMarkovChain_of_append reduces the Markov chain to the append identity h_app μ.map ((X,Y),U) = (μ.map (X,Y)) ⊗ₘ (prodMkRight β Q), discharged as a finite-support measure identity on singletons (compProd_apply + the dirac-sum lintegral + the auxiliary marginalization ∑_u q(x,y,u) = P_XY(x,y)). @audit:ok (the append identity h_app genuinely consumes the factorization hκeq q = κ(u|x)·P_XY; an arbitrary non-factorizable q would break it, so the chain is in the exact orientation mutualInfo_le_of_markov needs, not vacuous.)

Data-processing non-negativity of the Wyner–Ziv objective. On the factorizable manifold the auxiliary U sits atop the Markov chain U − X − Y (IsWynerZivFactorizable_markov), so the data-processing inequality gives I(Y;U) ≤ I(X;U), i.e. the objective I(X;U) − I(Y;U) is non-negative. This is the uniform (in the auxiliary alphabet size) lower bound 0 that makes the reshaped rate wynerZivRate non-degenerate.

h_pmf (the source is a genuine pmf) is a regularity precondition: it makes the factorizable joint q a pmf realizable as a probability measure. Nonempty V holds automatically at every non-empty-constraint index (row-stochasticity of the kernel forces V non-empty).

The proof realizes q as the discrete measure μ = wzPmfMeasure q on α × β × V with coordinate projections; the objective is landed onto (mutualInfo μ X U).toReal − (mutualInfo μ Y U).toReal via the pmf↔measure bridges wzMutualInfoXU_eq_mutualInfo / wzMutualInfoYU_eq_mutualInfo; the measure-form data-processing inequality mutualInfo_le_of_markov is applied with the Markov chain Y − X − U (wzFactorizable_isMarkovChain) read off the factorization q = κ(u|x)·P_XY, and ENNReal.toReal_mono finishes. @audit:ok (hq is the domain constraint defining the factorizable manifold — it supplies the Markov structure, not the conclusion. Sufficiency: dropping hq makes the claim false (a q with U depending on Y gives I(Y;U) > I(X;U)), so it is necessary, not under-hypothesized; h_pmf / Nonempty V are regularity preconditions.)

The reshaped value set wzRateValueSet is bounded below by 0 when the source is a pmf. This discharges the BddBelow guard of the reshaped rate, certifying non-degeneracy: every objective value is ≥ 0 by the data-processing non-negativity wzObjective_nonneg_of_factorizable, so the sInf cannot collapse to a junk ≤ 0.

@audit:ok (the k = 0 exfalso (row-stochasticity ∑_{Fin 0} κ = 0 ≠ 1) is a genuine impossibility argument, not a vacuous-truth shortcut; the BddBelow guard rests on the DPI input wzObjective_nonneg_of_factorizable.)