A per-slack, per-n good deterministic Wyner–Ziv code. Consuming the same covering data as the capstone wz_perDelta_covering_binning, produce for every block length n a Wyner–Ziv code at the operational rate R (codebookSize R n messages), together with a single threshold N beyond which the code's expected block distortion is within D + δ.

The body is the rate-split glue: the rate identity wz_mutualInfo_restriction_eq picks an intermediate covering rate R₁ ∈ (I(X;U), …) with R₁ − I(Y;U) < R, feeds the covering family hcov at R₁, and hands the whole per-n construction to the giant wz_perN_covering_binning_code, which bins the covering index to codebookSize R n messages (wzIndexBinningMeasure), decodes by the bin conditional-typicality search (wzBinTypicalDecoder) reconstructing γ^n via wzCodeOfCoveringBinning, bounds the covering-failure (wz_covering_failure_prob_le) and codebook-restricted decoder-confusion (wz_codebook_confusion_expectation_le, whose per-codeword mass upper bound is the AEP crux wz_covering_codeword_sideInfo_mass_le) error events, derandomizes (exists_codebook_low_avg / exists_pair_le_of_binning_integral_le), squeezes the distortion to D + δ (source_avg_distortion_le_simpler, ceil_exp_mul_exp_neg_tendsto_atTop), and extends the source α' → α (wzLiftSupportCode + wz_expectedBlockDistortion_source_agree).

The hypotheses are covering data / regularity: granting all 13 hands you a feasible test channel plus a covering LossyCode family at the covering rate R₁, not the binned Wyner–Ziv code at the operational rate R (the index binning, the bin decoder, and the confusion-error exponent are done in the body). hobj' is the rate objective and hfeas the distortion feasibility (preconditions on the test channel, not the operational conclusion); hcov is the separately-established rate-distortion covering result, not a restatement of this lemma's Wyner–Ziv claim. The conclusion is non-degenerate: ∃ c sits inside ∀ n, so for the infinitely many n ≥ N a genuinely good code is required.

Covering + binning capstone. Consuming the covering data (the full-support factorizable joint q' with kernel κ', the restricted covering joint qStar, the covering proxy distortion d', the covering feasibility hfeas, and the covering LossyCode family hcov), assemble the per-slack Wyner–Ziv code family at the operational rate R: bin the covering index down to codebookSize R n messages, decode by the bin conditional-typicality search, bound the covering-failure and codebook-restricted decoder-confusion error events, extract a good deterministic codebook

• binning by double derandomization (exists_codebook_low_avg / exists_pair_le_of_binning_integral_le), squeeze the residual distortion excess to 0 (source_avg_distortion_le_simpler, ceil_exp_mul_exp_neg_tendsto_atTop), and extend the covering code α' → α (wzLiftSupportCode + wz_expectedBlockDistortion_source_agree).

All hypotheses are covering data / regularity — the covering LossyCode family, the distortion feasibility, positivity and simplex membership. No error-probability or decoder-correctness claim is a hypothesis (those are derived in the body). Granting the 13 hypotheses does not hand you the binned Wyner–Ziv-code achievability: the binning, the bin decoder, and the confusion-error exponent remain genuine proof work, done in the body of wz_perDelta_covering_binning_eventual, over which this is the pure Filter.atTop/choice glue. hobj' is the rate objective (precondition, not the conclusion); hcov is the separately-established rate-distortion covering result, not a bundling of this lemma's own claim.

Existence of a Wyner–Ziv code sequence (at the operational message rate R) whose expected block distortion is eventually within D + ε.

The body is a reduction: wz_testChannel_of_rate_lt extracts a feasible factorizable test channel below R from the feasibility guard h_ne and h_rate, and wz_goodCode_exists_of_testChannel builds the code sequence from it.

The feasibility precondition h_ne (the rate-distortion value set is nonempty at D) makes the signature well-posed: it rules out the infeasible regime D below the min achievable distortion (e.g. any D < 0 for a NNReal distortion), where wzRateValueSet is empty and wynerZivRate = sInf ∅ = 0 would otherwise let h_rate : 0 < R coexist with a false existence claim. h_ne is a regularity/feasibility precondition, not the covering+binning core.

Wyner–Ziv operational achievability. If the information-theoretic Wyner–Ziv rate wynerZivRate at distortion D for the i.i.d. source P_XY (with decoder side information Y) is strictly below R, then R is operationally achievable at distortion D: there is a sequence of Wyner–Ziv block codes whose log-cardinality rate tends to R and whose expected block distortion is eventually within D + ε for every ε > 0.

The body is assembled: the message sequence is fixed to codebookSize R n = ⌈exp(n R)⌉, whose log-cardinality rate tends to R via codebookSize_log_div_tendsto (using 0 < R, from wynerZivRate_nonneg and h_rate); the distortion sequence is supplied by the covering + binning construction wyner_ziv_achievability_codes. The signature carries the same feasibility precondition h_ne as the codes lemma, so it is well-posed.