Single-letterization core of the Wyner–Ziv converse (feasible-point form).

For a block Wyner–Ziv code on an i.i.d. source (Xⁿ, Yⁿ) with expected block distortion at most D, there is a single-letterized feasible factorizable point — at some finite auxiliary alphabet Fin k — whose Wyner–Ziv objective I(X;U) − I(Y;U) is bounded by the per-symbol block mutual-information difference (1/n)(I(J; Xⁿ) − I(J; Yⁿ)).

This is the analytic heart of the converse (Cover–Thomas): the auxiliary Uᵢ := (J, Y_{\i}) gives, via the conditional mutual-information chain ∑ᵢ [I(Xᵢ;Uᵢ) − I(Yᵢ;Uᵢ)] = ∑ᵢ I(Xᵢ;Uᵢ|Yᵢ) = ∑ᵢ I(Xᵢ;J|Yⁿ) ≤ I(Xⁿ;J|Yⁿ) = I(J;Xⁿ) − I(J;Yⁿ) (not the heterogeneous Csiszár sum identity, which is orphaned on this route) and per-letter feasibility from the memoryless source (Markov Uᵢ − Xᵢ − Yᵢ, wz_perletter_markov), the sum bound ∑ᵢ [I(Xᵢ;Uᵢ) − I(Yᵢ;Uᵢ)] ≤ I(J;Xⁿ) − I(J;Yⁿ); the time-sharing auxiliary U* = (Q, U_Q) (with Q uniform on the time index Fin n) assembles the per-letter points into one factorizable point of distortion (1/n) ∑ᵢ Dᵢ ≤ D (from hD) and objective (1/n) ∑ᵢ [I(Xᵢ;Uᵢ) − I(Yᵢ;Uᵢ)].

Landing this point via wynerZivRate_le_of_feasible (with BddBelow supplied by wzRateValueSet_bddBelow_of_pmf) yields the converse bound in wyner_ziv_converse_n_letter_singleLetter; that outer landing is discharged (sorry-free) from this existence.

hindep (memoryless source) / hlaw (identical marginals = P_XY) / hD (distortion budget) are regularity preconditions — the construction (Markov Uᵢ − Xᵢ − Yᵢ, distortion budget (1/n)∑Dᵢ ≤ D) is false without them. The conclusion is the existence of a feasible witness realizing the objective bound; it is strictly weaker than the outer infimum bound (wynerZivRate ≤ …, recovered by landing), so this is a decomposition of the single-letterized core, not a restatement of it and not a hypothesis bundle.

The feasible-point existence is discharged by landing the uniform time-share of the per-letter witnesses supplied by wz_converse_perletter_witness — wzRateValueSet_avg_mem averages the per-letter values (1/n) ∑ w i into a value of wzRateValueSet … ((1/n) ∑ Dv i), wzRateValueSet_mono_in_D (with (1/n) ∑ Dv i ≤ D) relaxes it to budget D, and mem_wzRateValueSet_iff unpacks the resulting membership into the feasible factorizable point at some Fin k. @audit:ok (the conclusion is an existential witness (feasible factorizable point + objective bound), not a hypothesis bundle; hindep/hlaw/hD are source-regularity preconditions, and the Carathéodory support reduction is not on this single-letterization route.)

Wyner–Ziv converse, n-letter single-letterized form (reshaped rate).

For a block Wyner–Ziv code c with a measurable deterministic encoder / decoder on an i.i.d. source of (X, Y) pairs (mutual independence hindep + identical marginals hlaw = P_XY), whose expected block distortion is at most D, the reshaped Wyner–Ziv rate is bounded by the block log-cardinality rate:

R_WZ(D) ≤ (1/n) · log M.

Here R_WZ = wynerZivRate is the reshaped operational rate — the infimum of the objective over feasible factorizable points at every finite auxiliary alphabet Fin k (FactorizableRate.lean §10). This ∀-clean form removes the Carathéodory sizing precondition hU_card : |α| + 1 ≤ |U| that the fixed-U wynerZivRateFactorizable version required: the single-letterization auxiliary Uᵢ := (J, Y_{\i}) (whose cardinality grows with n) lands directly as a feasible point of the reshaped infimum via wynerZivRate_le_of_feasible, with no cardinality bound.

The independence / i.i.d. preconditions (hindep + hlaw) are regularity preconditions (the conclusion is false without them, mirroring rate_distortion_converse_n_letter_singleLetter).

Proof: the block bound (I(J; Xⁿ) − I(J; Yⁿ)).toReal ≤ log M is discharged via mutualInfo_diff_le_log_card, and after the (1/n)-scaling the single-letterization step h_sl is discharged by landing the feasible-point existence wz_converse_feasible_point: wynerZivRate_le_of_feasible (with BddBelow from wzRateValueSet_bddBelow_of_pmf) turns "some feasible factorizable point at Fin k has objective ≤ (1/n)(I(J;Xⁿ) − I(J;Yⁿ))" into R_WZ(D) ≤ (1/n)(I(J;Xⁿ) − I(J;Yⁿ)).toReal. No Carathéodory support lemma is on this critical path.

Dropping hU_card is sound: wynerZivRate is the infimum over the union of images across all Fin k, hence ≤ any single fixed-U rate, i.e. the weakest (smallest-LHS) converse claim — the single-letterization auxiliary lands directly, so no sizing precondition is needed and no false-statement is introduced. Non-vacuous: wynerZivRate ≥ 0 via the DPI residual, and M ≥ 1 ⟹ log M ≥ 0, so R_WZ(D) ≤ (1/n) log M is a substantive bound. hindep / hlaw are i.i.d. regularity preconditions (conclusion false without them), not a bundled core. @audit:ok (hindep/hlaw/hD + measurability are operational-regularity preconditions and the converse core is proved in the body, not bundled; dropping hU_card is a strengthening since wynerZivRate is the infimum over all Fin k, so no false-statement is introduced.)

Per-code converse bound (i.i.d.-source realization). For a single block Wyner–Ziv code c : WynerZivCode M n α β γ with expected block distortion at most D, the reshaped Wyner–Ziv rate is bounded by the block log-cardinality rate (1/n) · log M.

This is the i.i.d.-source plumbing of the converse: the canonical i.i.d. source is the product measure Measure.pi (fun _ ↦ P_XY) on (α × β)^n with coordinate projections Xs i ω := (ω i).1, Ys i ω := (ω i).2, whose independence and identical marginals (= P_XY) are supplied by iIndepFun_iff_map_fun_eq_pi_map and Measure.pi_map_eval. The bound is then the n-letter single-letterized converse wyner_ziv_converse_n_letter_singleLetter.