Joint pmf induced by a transition kernel κ : α → U → ℝ and source P_XY: q(x, y, u) = κ x u · P_XY (x, y).

The set of row-stochastic transition kernels α → U → ℝ (per-row non-negative, per-row sum 1) — a product of standard simplices, hence compact.

Feasible kernels at distortion budget D: row-stochastic kernels admitting a side-information decoder whose expected distortion is within the budget.

wzJointOfKernel is continuous in the kernel κ.

A row-stochastic kernel induces a factorizable joint.

The kernel set is compact (a product of standard simplices).

Expected distortion is continuous in the joint pmf q.

The feasible kernel set is closed.

The feasible kernel set is compact.

The feasible kernel set is monotone in the distortion budget.

Kernel-space form of the factorizable rate: the factorizable rate equals the infimum of the Wyner–Ziv objective over feasible kernels (a compact set).

Fixed-U right-continuity of the factorizable rate. If the rate at every D + ε (ε > 0) is ≤ R, then so is the rate at D. Proved by compactness: near-optimal feasible kernels at D + εₙ live in the compact kernel set; Cantor's intersection theorem produces a common limit kernel, feasible at D (a decoder attaining the budget survives to the limit) with objective ≤ R.

The Wyner–Ziv objective I(X;U) − I(Y;U) evaluated on the joint pmf induced by a kernel κ. This is the kernel-space form of the objective minimized by wynerZivRateFactorizable.

The objective image over the factorizable constraint set equals the objective image over the feasible kernel set (the extensional form of the himg step inside wynerZivRateFactorizable_eq_sInf_kernel).

The reshaped value set is the union, over all finite auxiliary alphabets Fin k, of the kernel-space objective images. Kernel-space form of wzRateValueSet.

Entropy-mixture identity. The kernel-space Wyner–Ziv objective splits as the source marginal-entropy difference H(X) − H(Y) plus the sum over auxiliary letters of the per-u conditional-entropy-difference block ∑_y neg(m_YU(y,u)) − ∑_x neg(m_XU(x,u)). The auxiliary-marginal entropy terms ∑_u neg(P_U u) in I(X;U) and I(Y;U) cancel, leaving the block sum. This is the affine functional (in the per-letter mixture) that the Carathéodory support reduction acts on. @audit:ok (algebraic identity by Finset.sum_comm / sum_sub_distrib / ring; hκ is row-stochasticity regularity — used only to fold the joint's (X,Y)-marginal back to P_XY and to cancel H(U) — not a bundled core.)

Carathéodory support reduction. Any feasible factorizable kernel at an arbitrary finite auxiliary alphabet Fin k reduces to a feasible kernel at the fixed alphabet Fin (|α| + 3) with objective ≤ the original.

Encode each auxiliary letter u with P_U(u) > 0 by the vector Φ_u = (P_{X|U=u}, g_u, δ_u) ∈ ℝ^{|α|+2} (coordinates indexed by α ⊕ Bool), where P_{X|U=u}(x) = m_XU(x,u)/P_U(u), the objective density g_u = block_u(κ)/P_U(u) with block_u(κ) = ∑_y neg(m_YU(y,u)) − ∑_x neg(m_XU(x,u)), and the distortion density δ_u = dist_u/P_U(u). The P_U-weighted mixture M = ∑_u P_U(u) Φ_u = (P_X, objective−(H(X)−H(Y)), distortion) lies in convexHull (range Φ) ⊆ ℝ^{|α|+2}, so by bare Carathéodory (eq_pos_convex_span_of_mem_convexHull + card_le_finrank_succ, with finrank ℝ (α ⊕ Bool → ℝ) = |α|+2) it is a convex combination of at most |α|+3 of the Φ_u. This deliberately relaxes the target size to |α|+3 (rather than the tighter |α|+2, which would need the vectorSpan hyperplane refinement ∑ P_{X|U=u} = 1, or the Fenchel–Eggleston |α|+1 improvement absent from Mathlib): the K-agnostic endpoint assembly (wynerZivRate_le_of_forall_pos_add_endpoint) makes this non-load-bearing, and a larger-than-tight K only eases the ∃-claim, never falsifies it.

h_pmf (simplex membership) and hκ (the input feasible kernel — the data being reduced) are preconditions, not a *Hypothesis/*Reduction predicate bundling the reduction's core.

Proof: assembled from four pieces.

• Entropy-mixture identity wzKernelObjective_eq_blockSum: wzKernelObjective V P_XY κ = (H(X) − H(Y)) + ∑_u block_u(κ).
• Mass equality: both letter marginals total P_U u (∑_x m_XU(x,u) = P_U u = ∑_y m_YU(y,u)), the identity that makes the block-scaling corrections cancel.
• Convex geometry wz_caratheodory_reduce (bare Carathéodory + zero-padding reindex wz_fin_pad_sum): reduces M ∈ convexHull (range Φ) to weights λ_j on letters u_j = σ j.
• Kernel reconstruction — κ'(x,j) = (λ_j/P_U(u_j))·κ(x,u_j) on P_X(x) > 0 rows (with a fixed-pmf override on P_X(x)=0 rows, invisible since P_XY(x,·)=0 there); decoder slice f'(j,·) = f(u_j,·). Feasibility (distortion' = distortion ≤ D, via the δ-coordinate) and objective equality (objective' = objective, via the g-coordinate + the block-scaling block_j(κ') = (λ_j/P_U(u_j))·block_{u_j}(κ) from Real.negMulLog_mul + mass equality) are proved directly, so objective' = objective, whence ≤. @audit:ok (non-circular and non-bundled: h_pmf is simplex regularity, hκ the input datum being reduced, and the conclusion ∃ κ' : Fin (|α|+3) feasible with objective ≤ is not a hypothesis restated; the objective is proven equal — stronger than ≤ — and distortion preserved exactly, so the reduction genuinely follows.)

Carathéodory fixed-K identification of the reshaped Wyner–Ziv rate. The reshaped rate wynerZivRate (an infimum over all finite auxiliary alphabets) is attained already at the fixed auxiliary alphabet Fin (|α| + 3): every feasible factorizable point at any Fin k reduces, by the Carathéodory support reduction wz_support_reduce (the rate-optimal auxiliary mixes at most |α| + 3 extreme kernels), to a feasible point at Fin (|α| + 3) with objective ≤ the original. Hence the two infima agree.

The auxiliary size is |α| + 3 (bare ambient Carathéodory in ℝ^{|α|+2}); the endpoint assembly that consumes this identification is K-agnostic, so this choice is non-load-bearing.

Both sInf inclusions are proved here, reduced to the single core lemma wz_support_reduce:

• ≥ (sInf S_K ≤ sInf(⋃ T_k)): every union witness reduces (via wz_support_reduce) into S_K with objective ≤, so sInf S_K lower-bounds the union.
• ≤ (sInf(⋃ T_k) ≤ sInf S_K): S_K = T_K ⊆ ⋃ T_k, so csInf_le_csInf; the sInf ∅ = 0 collapse is handled by the nonemptiness equivalence ⋃ T_k ≠ ∅ ↔ S_K ≠ ∅ (⟸ trivial since S_K ⊆ ⋃; ⟹ via the same reduction), so both infima are 0 in the empty case. This is exactly why the ≤ direction is not free — the reduction is what guarantees the fixed-K set is nonempty whenever the union is. @audit:ok (a genuine equality of two infima: ≤ from B ⊆ A (csInf_le_csInf), ≥ from wz_support_reduce landing every union witness into B with objective ≤; K = |α|+3 is the minimal size for hcardK, and a too-small K would break ≥, so it is true as-framed, not vacuous.)

Left-endpoint right-continuity of the reshaped Wyner–Ziv rate.

If R ≥ 0, the value set at D is nonempty but no value set strictly below D is nonempty (so D is the left endpoint D_min of the rate function's domain), and R_WZ(D + ε) ≤ R for every ε > 0, then R_WZ(D) ≤ R.

The body assembles wynerZivRate_eq_factorizable_finK (the Carathéodory fixed-K identification) and wynerZivRateFactorizable_right_continuous_le (fixed-U right-continuity via compactness): the former rewrites R_WZ(·) to the fixed-Fin (|α|+3) factorizable rate at both D and each D + ε, and the latter closes the goal.

Why the conclusion is genuine (not vacuous, not false-as-framed): R_WZ is antitone, so R_WZ(D + ε) ≤ R_WZ(D) (the wrong direction) and hstep alone does not force R_WZ(D) ≤ R; one needs right-continuity R_WZ(D) = lim_{ε→0⁺} R_WZ(D + ε). The abstract monotone-limit implication is false (a convex antitone function may jump up at the left endpoint), but the signature names the concrete wynerZivRate, whose fixed-K form wynerZivRateFactorizable (Fin (|α|+3)) is an infimum over a compact set of kernels with a continuous objective. For each ε, the fixed-K infimum is attained by a feasible kernel with objective ≤ R; these live in one compact kernel set, so Cantor's intersection theorem produces a common limit kernel, feasible at D (its best decoder's distortion survives the ε → 0 limit) with objective ≤ R, whence R_WZ(D) ≤ R.

hR (0 ≤ R, handling the S(D) = ∅ ⟹ sInf = 0 boundary) and hstep (the right-continuity input) are used; h_ne and h_endpoint are not needed by the compactness proof (it holds at every D, not only the left endpoint) but are retained as declared preconditions, so this is a stronger claim (proved from fewer assumptions); none is load-bearing. @audit:ok (the retained-but-unused h_ne/h_endpoint strengthen the claim, not bundle a core; hR/hstep are genuine preconditions and the conclusion follows via compactness.)

Wyner–Ziv converse (Cover–Thomas, operational lower bound).

If rate R is achievable at distortion D for the i.i.d. source P_XY with decoder side information, then the reshaped Wyner–Ziv rate satisfies R_WZ(D) ≤ R.

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 is the ∀-clean form of the converse: it carries no auxiliary sizing precondition. The earlier fixed-U wynerZivRateFactorizable U form was false-as-framed for a too-small U (its sInf is antitone in |U|, so a U below the Carathéodory threshold |α| + 1 restricts the infimum strictly above the achievable R), which forced the sizing precondition hU_card. Taking the infimum over all finite auxiliary alphabets removes that false-statement risk at the source: the reshaped sInf is over the union of images across all Fin k, so a large single-letterization auxiliary lands directly (no Carathéodory reduction).

Non-degeneracy: wynerZivRate is sInf (wzRateValueSet …), guarded against the junk sInf ∅ = 0 collapse by the data-processing non-negativity of the objective (wzObjective_nonneg_of_factorizable → wzRateValueSet_bddBelow_of_pmf); the source pmf lies in the simplex by measureReal_pmf_mem_stdSimplex. So sInf ≤ R is a genuine bound, not vacuously true.

Proof: from h_ach extract the code sequence, then establish 0 ≤ R (M n ≥ 1 ⟹ log (M n) ≥ 0, ge_of_tendsto); ∀ ε > 0, R_WZ(D + ε) ≤ R by applying the n-letter converse wyner_ziv_converse_n_letter_singleLetter to the canonical i.i.d. source Measure.pi (fun _ ↦ P_XY) (via wynerZivRate_le_of_code) and passing (1/n) log (M n) → R through ge_of_tendsto; then the limit ε → 0⁺, split on the value set at D:

• S(D) = ∅ gives R_WZ(D) = sInf ∅ = 0 ≤ R;
• an anchor D₀ < D with S(D₀) nonempty gives the bound by the time-sharing perturbation wzRateValueSet_timeShare_mem plus t(ε) → 0;
• the left-endpoint case (h_endpoint) is discharged by wynerZivRate_le_of_forall_pos_add_endpoint.

Dropping hU_card is sound: wynerZivRate = inf over all finite auxiliaries is the weakest converse claim, so R_WZ(D) ≤ R follows without a sizing precondition and is non-vacuous (bounded below by 0 via the DPI residual, and R ≥ 0 in the achievable regime). The case split on D is exhaustive and disjoint. @audit:ok (h_ach : WynerZivAchievable is the operational antecedent (∃ codes), consumed via obtain + ge_of_tendsto, not the conclusion bundled — dropping it would let R be arbitrary; the conclusion is non-vacuous since wynerZivRate is an sInf bounded below by 0 via the DPI wzObjective_nonneg_of_factorizable.)