Wyner–Ziv side-information decoder confusion bound. For a random binning f of the covering-codeword space Fin n → U into M bins, the expected μ-probability (over the binning f ∼ binningMeasure U n M) that some codeword u' ≠ U^n that is jointly typical with the received side information Y^n hashes to the same bin as the true codeword U^n is at most exp(n · (H(U|Y) + 2ε)) / M.

This is the decoder-confusion half of Wyner–Ziv achievability. It is the side-information analogue of the Slepian–Wolf alias bound, with the covering codeword U in the source role and the side information Y as the conditioning variable; the proof is a direct instantiation of swError_EX_expectation_le, witnessing that the binning ∘ conditional-typicality composition closes as plumbing over an existing atom. @audit:ok

Wyner–Ziv covering acceptance mass bound. For a strongly-typical covering codeword u : Fin n → U, the product Y-mass of the fiber of side words jointly strongly typical with u is bounded below by exp(−n · (H(U) + H(Y) − H(U,Y) + slack)), i.e. exp(−n · (I(U;Y) + slack)). This is the covering-acceptance half of Wyner–Ziv achievability: the correct covering codeword is conditionally typical with the side information with high probability. Direct instantiation of conditionalStronglyTypicalSlice_mass_ge. @audit:ok

The reshaped Wyner–Ziv rate for a probability-measure source is ≥ 0. Via Real.sInf_nonneg, every value of the rate set is the objective of a feasible factorizable point, which is ≥ 0 by the data-processing inequality wzObjective_nonneg_of_factorizable; a feasible factorizable point forces k > 0 (a Fin 0 kernel has row-sum ∑_{u:Fin 0} κ x u = 0 ≠ 1). The bound holds even in the empty-feasible-set regime (0 ≤ sInf ∅ = 0), where Real.sInf_nonneg's premise is vacuously satisfied. @audit:ok

Witness extraction. From the feasibility guard h_ne and the rate strict inequality h_rate, extract a concrete finite auxiliary alphabet Fin k, a factorizable test channel qf feasible at distortion D, whose Wyner–Ziv objective I(X;U) − I(Y;U) is strictly below R.

This is exists_lt_of_csInf_lt on the infimum-of-values definition of wynerZivRate (= sInf (wzRateValueSet …)), with the resulting value unpacked by mem_wzRateValueSet_iff into a feasible factorizable point. exists_lt_of_csInf_lt requires h_ne (value set nonempty), so sInf < R is realized by an actual value; no vacuous sInf ∅ shortcut. @audit:ok

Nonempty auxiliary alphabet. A Wyner–Ziv factorizable joint over a source pmf on α × β forces a nonempty covering alphabet Fin k: the row-stochastic kernel condition ∑_{u : Fin k} κ x u = 1 is impossible for k = 0 (the empty sum is 0 ≠ 1), using Nonempty α to pick a row x.

Full-support kernel perturbation. From a feasible factorizable test channel qf (row-stochastic kernel, distortion ≤ D) whose Wyner–Ziv objective is strictly below R, and any slack δ > 0, produce a perturbed factorizable channel q' with a strictly positive kernel κ' (full support), whose objective is still < R and whose distortion is ≤ D + δ.

The perturbation is q' := (1 - τ) • qf.1 + τ • q_unif with q_unif the uniform-kernel factorizable joint and τ ∈ (0, 1] small: convex combination preserves factorizability (IsWynerZivFactorizable_convex_combination) and distortion feasibility (WynerZivFactorizableConstraint_convex_combination), the kernel κ' = (1 - τ) κ + τ/k ≥ τ/k > 0 gains full support, and continuity of the objective (continuous_wzObjective) keeps it < R for small τ.

Note this yields full support of the kernel, hence full support of the (X, U) joint marginal wzMarginalXU q' only on {x | 0 < P_X x} (the construction lemma restricts the source alphabet to this support): wzMarginalXU q' (x,u) = κ'(x,u)·P_X(x).

Message-count decay adapter. For c < R, the ratio exp(n c) / codebookSize R n → 0 as n → ∞. This is the E2 decoder-confusion decay term (collision mass over the bin count). Re-proved locally here because the Slepian–Wolf original tendsto_exp_mul_codebookSize_inv is private to PairBound.lean; the proof is a squeeze_zero against exp(n (c − R)) using (codebookSize R n)⁻¹ ≤ exp(−n R) from Nat.le_ceil.

Restricted covering joint, full support. From a strictly positive row-stochastic kernel κ' and the source marginal P_X x = ∑_y P_XY(x,y), the (X, U) joint κ'(x, u) · P_X(x) restricted to the support subtype α' := {x // 0 < P_X x} is a strictly positive pmf on α' × Fin k:

• α' is nonempty (a probability measure cannot have every row of P_X vanish);
• the joint is strictly positive on α' × Fin k (both factors are positive there);
• it lies in the standard simplex (row-sums collapse to ∑_{x' : α'} P_X(x'.1) = 1, the zero atoms of P_X contributing nothing).

This is the global-full-support source the rate-distortion covering theorem rate_distortion_achievability hard-requires (hqStar_pos), obtained on the restricted alphabet because factorizability forces P_X's zero atoms into the joint regardless of κ'. @audit:ok

Source-support block-distortion reconciliation. Two Wyner–Ziv codes that decode identically on every source sequence hitting only support atoms of P_X have equal expected block distortion, because Measure.pi P_XY assigns zero mass to sequences reaching a zero atom of P_X. This is the null-set transport that lets a code built on the support subtype α' := {x // 0 < P_X x} extend to a code on the full alphabet α without changing its distortion.

hagree is a genuine agreement precondition (not a bundled covering bound); the conclusion is the measure-level distortion equality only.

Strong-typicality ⟹ distortion-typicality bridge for the rdAmbient source. A joint strongly typical pair (x, y) (within ε_join) is entropy-typical on all three axes and its empirical block distortion is within δ_typ of the expected distortion, provided the three axis slacks fit under ε_dist and the aggregate distortion drift fits under δ_typ. Used to discharge the covering theorem's h_jts_subset_dts premise.

Rate-distortion covering layer. For a strictly positive joint pmf qStar on α' × Fin k with mutualInfoPmf qStar < R₁ and a proxy distortion d' feasible at D, the rate-distortion achievability theorem yields, for all large block lengths n, a lossy code with ≥ ⌈exp(n R₁)⌉ codewords whose expected block distortion (under the rdAmbient-pushed source) is within D + ε'.

The full support hpos is a regularity precondition (the covering theorem's hqStar_pos); the rate-distortion slack quintet (ε_X … δ_typ, qZ_min) is constructed in the body, not exposed. The reconciliation between the covering proxy d' (X↔U) and the Wyner–Ziv distortion (X↔γ) stays load-bearing in the body / (BD), never bundled into a predicate.

Covering-distortion reconciliation identity. The covering proxy distortion d' on the source-support subtype α' := {x // 0 < P_X x}, defined as the Y-conditional expectation d'(⟨x, _⟩, u) := ∑_y (P_XY(x,y) / P_X x) · d(x, f(u, y)), reconciles with the Wyner–Ziv distortion functional: for the restricted (X, U)-joint qStar(⟨x, _⟩, u) := κ'(x, u) · P_X x, the pmf-form expected distortion of d' equals the Wyner–Ziv expected distortion of the factorizable joint q'(x, y, u) := κ'(x, u) · P_XY(x, y) under the reconstruction f.

The identity is the load-bearing bridge that lets the rate-distortion covering theorem (which measures distortion X ↔ U via d') discharge the Wyner–Ziv feasibility (X ↔ γ via f). It holds because P_X x · (P_XY(x,y) / P_X x) = P_XY(x,y) on the support (where P_X x > 0), and the zero atoms of P_X contribute nothing on either side (q' vanishes there since every P_XY(x,y) = 0 when P_X x = 0). @audit:ok

The (U, Y)-marginal joint pmf feeding the side-information ambient, restricted to the positive-Y-marginal subtype. For a full-support covering kernel κ' and the source law P_XY, the value at (u, y) is ∑ₓ κ'(x, u) · P_XY{(x, y)}, the Y-side analogue of the covering pmf qStar (which lives on the positive-X-marginal subtype).

Covering-acceptance failure event. For a covering LossyCode c on the source-support subtype α' := {x // 0 < P_X x}, the set of block source–side pairs p : Fin n → α' × β whose true covering codeword c.decoder (c.encoder x) is not jointly (strongly) typical, at radius ε, with the side information y in the side-information ambient rdAmbient (wzSideInfoMarginal P_XY κ'). This is the covering half of the Wyner–Ziv error event E2: acceptance failure of the correct covering word (wzBinTypicalDecoder_eq_of_unique requires this joint typicality to recover it), so C2 ⊆ E2. Pure event set (data), used to state the covering-acceptance-failure mass bound threaded from the covering construction to wz_exists_binning_E2_bound (A3).

The source–side covering pmf (x', y) ↦ P_XY{(x'.1, y)} (on the source-support subtype) is a probability vector: its values are nonnegative measures and they total 1 (the zero-P_X atoms carry no mass, so the subtype sum equals the full joint mass). Used to supply the IsProbabilityMeasure instance for the correlated-joint source measure Measure.pi (pmfToMeasure …).

The n-fold pair-sequence law of rdAmbient q is the product of the pmf q: the joint (X, Y)-sequence jointRV (jointSequence iidXs iidYs) n pushes rdAmbient q to Measure.pi (pmfToMeasure q). The iid-to-product identity for the pair sequence (the jointSequence analogue of wz_ambient_jointRV_iidYs_eq_pi).

Per-atom mass is preserved by pushing forward along an injective (measurable) alphabet map: (μ.map (g ∘ X)).real {g a} = (μ.map X).real {a}.

Shannon entropy is invariant under an injective (measurable) relabeling of the alphabet.

The Wyner–Ziv source per-coordinate pmf p ↦ P_XY{(p.1.1, p.2)} on α' × β is a pmf.

Side-information-law agreement: the source's full-β Y-law equals the β-image (under the subtype coercion) of the ambient's β'-Y-law.

The n-fold side-information law of the ambient factorizes as the product of its single-letter β'-Y-marginal.