Affine factorization predicate. The joint pmf q : α × β × U → ℝ is Wyner–Ziv factorizable over the source P_XY : α × β → ℝ if there exists a transition kernel κ : α → U → ℝ (per-row non-negative and per-row sum 1) such that

q(x, y, u) = κ(u | x) · P_XY(x, y).

This is the affine re-parameterization underlying Cover–Thomas; the quadratic Markov cross-product constraint is automatically satisfied (see IsWynerZivFactorizable_markov below).

Membership unfold for IsWynerZivFactorizable.

Markov chain holds automatically on factorizable joints. The quadratic cross-product equation collapses to a kernel-level identity that is trivially symmetric in u, u'.

(X, Y)-marginal of a factorizable joint recovers P_XY (when the kernel κ is row-stochastic).

Factorizable joints are non-negative pointwise (when P_XY is).

Total mass of a factorizable joint equals total mass of P_XY. When P_XY is a pmf (total mass 1), the joint is also total-mass 1.

stdSimplex membership for factorizable joints over a pmf source. If P_XY ∈ stdSimplex (a pmf), then every factorizable joint is also in stdSimplex ℝ (α × β × U).

Convex combinations of factorizable joints are factorizable. This is the key affine property that re-parameterization buys us: although the Markov cross-product constraint is non-affine on the raw joint pmf coordinate, on the factorized manifold the predicate is affine in κ, and the kernel-level convex combination

κ := a • κ₁ + b • κ₂

is again row-stochastic (non-negativity + row-sum 1). The joint combination then factors:

a • q₁ + b • q₂ = (a • κ₁ + b • κ₂) ⊗ P_XY.

Factorizable Wyner–Ziv constraint set. A (q, f) pair belongs iff:

1. q is IsWynerZivFactorizable U P_XY — factorizes as κ(u|x)·P_XY(x,y),
2. wzExpectedDistortion d q f ≤ D — distortion budget.

The simplex / marginal / Markov constraints (1-3 of WynerZivConstraint) are consequences of the factorization predicate when P_XY is itself a pmf; we record this as the factorisable_subset_constraint lemma below.

Membership unfold for WynerZivFactorizableConstraint.

Factorizable constraint ⊆ raw constraint. Every factorizable feasible point is also feasible in the original (un-re-parameterized) constraint set, provided P_XY is itself a pmf in the simplex.

Factorizable constraint set is monotone in D. Mirror of WynerZivConstraint_mono_in_D.

A convex combination of two factorizable feasible points at thresholds D₁, D₂ is feasible at the mixed threshold a D₁ + b D₂, with the decoder f shared between the two points.

This is the structural step that turns convexity into a one-liner on factorizable joints: feasibility survives convex combinations on the factorized manifold (unlike the raw constraint set where the Markov cross-product fails to be preserved).

Wyner–Ziv rate function restricted to factorizable joints. R_WZ_fact(D) := sInf { I(X;U) − I(Y;U) | (q, f) ∈ WynerZivFactorizableConstraint U P_XY d D }.

This is the form Cover–Thomas directly addresses: the minimization over auxiliary kernels κ(u|x) with side-information decoders f(u,y).

Factorizable rate is antitone in D (mirror of the raw wynerZivRatePmf_antitone).

Convexity of the factorizable rate function along a fixed decoder f: under convexity of the objective on factorizable joints (h_obj_convex), feasibility witnesses at D₁, D₂, and BddBelow of the factorizable image at the mixed threshold, the inf over the mixed budget is bounded by the convex combination of objective values.

@audit:superseded-by(wynerZivRateFactorizable_convex_in_D)

The factorizable image is BddBelow. Same simplex-projection route as in WynerZiv/RateMonotonicity.lean: the factorizable image is contained in the raw image (modulo the side conditions in factorisable_subset_constraint), which is contained in objective '' stdSimplex, which is compact and hence bounded below.

The simplex-projection corollary of wynerZivRateFactorizable_convex: when P_XY ∈ stdSimplex, the BddBelow side condition is discharged via wynerZivFactorizableObjective_image_bddBelow, leaving the objective-convexity hypothesis and two feasibility witnesses.

@audit:superseded-by(wynerZivRateFactorizable_convex_in_D)

Convexity of the factorizable rate function in D, rate-level form: R_WZ_fact(a D₁ + b D₂) ≤ a · R_WZ_fact(D₁) + b · R_WZ_fact(D₂). Takes P_XY a pmf, objective convexity on factorizable joints, feasibility witnesses, and attainment of R_WZ_fact(Dᵢ) at those witnesses.

@audit:superseded-by(wynerZivRateFactorizable_convex_in_D)

The set of Wyner–Ziv objective values I(X;U) − I(Y;U) attainable by a factorizable feasible point at some finite auxiliary alphabet Fin k, with k ranging over all of ℕ. Feasibility-empty indices contribute the empty image (no value), so this set carries no junk sInf ∅ = 0 term.

Reshaped Wyner–Ziv operational rate: the infimum of the objective I(X;U) − I(Y;U) over feasible factorizable points at every finite auxiliary alphabet Fin k at once, rather than a single caller-fixed U.

This is the ∀-clean form needed by the operational converse: the single-letterization auxiliary lands directly as a feasible point (see wynerZivRate_le_of_feasible), with no Carathéodory cardinality reduction.

The union-of-images form wzRateValueSet avoids the junk sInf ∅ = 0 collapse — an empty-constraint index k (e.g. Fin 0) contributes the empty image to the ⋃, injecting no 0, so wynerZivRate ≤ R is a substantive claim (NOT the degenerate ⨅ k, sInf(image_k) form that would inject 0s). @audit:ok

Membership in wzRateValueSet: a real v is a value iff it is the objective of a feasible factorizable point at some finite auxiliary alphabet Fin k.

A feasible factorizable point at auxiliary alphabet Fin k produces a value in wzRateValueSet (witness for non-emptiness).

Any feasible factorizable point at auxiliary alphabet Fin k bounds the reshaped rate from above. This is what lets the single-letterization auxiliary land directly, with no cardinality reduction. The BddBelow side condition is discharged (via the objective's data-processing non-negativity) in Converse.lean by wzRateValueSet_bddBelow_of_pmf.

sorryAx-free (#print axioms). hbdd : BddBelow … is a regularity precondition (the exact hypothesis of csInf_le), mirroring wynerZivRatePmf_le_of_feasible; it does NOT smuggle the proof core — the body is the standard csInf_le shape. @audit:ok

The reshaped value set is monotone in D: enlarging the distortion budget enlarges the set of attainable objective values, since every feasible factorizable point at budget D remains feasible at D' ≥ D (WynerZivFactorizableConstraint_mono_in_D, applied at each auxiliary alphabet Fin k).

sorryAx-free, #print axioms = [propext, Classical.choice, Quot.sound]; subset body via WynerZivFactorizableConstraint_mono_in_D, no load-bearing hyp / vacuity. @audit:ok

The reshaped Wyner–Ziv rate is antitone in D: a larger distortion budget enlarges the value set (wzRateValueSet_mono_in_D), so its infimum is smaller. The BddBelow at D' and non-emptiness at D are the standard csInf_le_csInf side conditions — both discharged in Converse.lean (via wzRateValueSet_bddBelow_of_pmf and a feasible witness).

sorryAx-free, #print axioms = [propext, Classical.choice, Quot.sound]; csInf_le_csInf body. h_bdd / h_ne are its standard regularity side conditions, not load-bearing core, and the antitone direction D ≤ D' ⟹ rate(D') ≤ rate(D) is the correct one. @audit:ok

Time-sharing helper. From X ≤ c · s for every s in a nonempty set S together with 0 ≤ c, conclude X ≤ c · sInf S. Isolates the c = 0 boundary from the c > 0 division step.

Total mass of the second marginal equals the total mass of the joint.

Pmf mutual information is affine under disjoint-union mixtures. For two joint pmfs p₁ : A × B₁ → ℝ and p₂ : A × B₂ → ℝ, each of total mass 1 and sharing the same first marginal (marginalFst p₁ = marginalFst p₂, i.e. I(X ; branch) = 0), form the disjoint-union mixture mix : A × (B₁ ⊕ B₂) → ℝ with

mix (x, inl b₁) = a · p₁ (x, b₁),   mix (x, inr b₂) = b · p₂ (x, b₂)

for weights a + b = 1. Then the pmf mutual information is affine:

mutualInfoPmf mix = a · mutualInfoPmf p₁ + b · mutualInfoPmf p₂.

The branch entropy H(a, b) cancels between the H(U) term and the H(X, U) term; the shared-first-marginal hypothesis is what kills the H(X)-side contribution. This is the reusable engine for Wyner–Ziv time-sharing (both the value-set closure and the operational converse feasible-point step).

@audit:ok sorryAx-free, #print axioms = [propext, Classical.choice, Quot.sound]. Signature honest: h₁sum/h₂sum are pmf total-mass-1 regularity, hmix₁/hmix₂ merely define the disjoint-union mixture (not the conclusion), hab is the weight normalization. h_marg (shared first marginal) is a precondition ON THE INPUTS — load-bearing for TRUTH (dropping it makes the identity false, since H(X) is concave not affine) yet NOT bundling the conclusion (the affine identity is a claim about the mixture's mutualInfoPmf, proven in-body via the H(a,b) branch-entropy cancellation). Coefficients a,b verified correct (right, not swapped); a=0/a=1 degenerate boundaries stay alive and true.

mutualInfoPmf is invariant under reindexing the second coordinate by an equivalence.

The objective value of a feasible factorizable point at any finite auxiliary alphabet U lands in wzRateValueSet — reindex U to Fin (Fintype.card U), under which factorizability, distortion, and the objective are all preserved.

The set of attainable Wyner–Ziv objective values is closed under time-sharing, that is, under convex combination across distortion budgets: if v₁ is attainable at budget D₁ and v₂ at budget D₂, then the mixture a·v₁ + b·v₂ is attainable at the mixed budget a·D₁ + b·D₂.

The witness is the disjoint-union auxiliary kernel κ(x, inl u) = a·κ₁(x, u), κ(x, inr u) = b·κ₂(x, u) at auxiliary alphabet Fin k₁ ⊕ Fin k₂: it is row-stochastic, its distortion splits as a·dist₁ + b·dist₂, and its objective is affine by mutualInfoPmf_mixture_affine.

@audit:ok sorryAx-free, #print axioms = [propext, Classical.choice, Quot.sound]. All hypotheses are convex-combination preconditions: h_pmf (P_XY a pmf, supplies total-mass-1 for the affine engine), hv₁/hv₂ (the input value-set memberships of a closure statement), ha/hb (weight non-negativity, feeds kernel non-negativity + distortion bound), hab (weight normalization, feeds row-stochasticity). NONE bundles the conclusion — the mixture kernel, its feasibility (row-stochastic + distortion budget), and the affine objective are all CONSTRUCTED/PROVEN in-body (~150 lines). The combined point lands at a Fin (k₁+k₂) index via wzRateValueSet_reindex_mem (not empty/degenerate). Stated over the reshaped ⋃-over-Fin k value set. Break attempts: a=0 reduces to hv₂ (alive, non-vacuous); D₁=D₂ gives midpoint time-sharing.

The reshaped Wyner–Ziv rate is convex in D. This follows directly from the time-sharing closure wzRateValueSet_timeShare_mem: every mixture a·v₁ + b·v₂ lies in the value set at the mixed budget, so its infimum is bounded above by a·v₁ + b·v₂ for all attainable v₁, v₂; taking nested infima gives the convex bound. The Nonempty side conditions feed le_csInf (via le_mul_csInf) and BddBelow at the mixed budget feeds csInf_le; both are standard regularity preconditions, not load-bearing core.

@audit:ok sorryAx-free, #print axioms = [propext, Classical.choice, Quot.sound]. Signature honest: h_ne₁/h_ne₂ are the Nonempty side conditions of le_csInf (via le_mul_csInf), h_bdd_mix is the BddBelow side condition of csInf_le — both standard infimum regularity (side conditions of the sInf lemmas, NOT the theorem's asserted value, mirroring the already-audited wynerZivRate_antitone). h_pmf feeds wzRateValueSet_timeShare_mem; ha/hb/hab are convex weights. The convexity content is proven in-body via the time-sharing closure + nested infima, not bundled. Convexity direction and coefficients verified correct; a=1,b=0 boundary reduces to reflexivity (alive), stated over the reshaped wynerZivRate.

Weighted (n-ary) time-sharing closure of the reshaped value set: a convex combination ∑ i, p i · w i of attainable objective values (each w i attainable at its own budget Dv i) is attainable at the mixed budget ∑ i, p i · Dv i. Proved by induction over the finite index set s from the binary closure wzRateValueSet_timeShare_mem, renormalizing the tail weights so the binary lemma applies at each induction step.

The average (1/n)·∑ᵢ w i of n attainable objective values is attainable at the averaged budget (1/n)·∑ᵢ Dv i. Uniform Fin n specialization of wzRateValueSet_weightedSum_mem at weights p ≡ 1/n; this is the form the operational converse consumes.