Wyner–Ziv code from a covering codebook + binning + bin decoder. The encoder covers the source with the covering codebook (c₁.encoder) and bins the covering index (f). The decoder reconstructs γ^n letterwise via rec (the test-channel decoder qf.2 : Fin k × β → γ) from the bin decoder's word dec (m, y) : Fin n → Fin k and the side information y. Pure assembly; the covering codebook c₁, the binning f, the reconstruction map rec and the bin decoder dec are all supplied.

Bin/side-information conditional-typicality decoder. Given a bin m and side information y, search the bin's covering codebook members {c₁.decoder m' | f m' = m} for the unique word jointly typical with y, returning that Fin n → Fin k word (falling back to an arbitrary word if none exists or the witness is not unique). The search ranges over codebook members only (indexed by the covering index m'), not over all Fin n → Fin k words — this restriction is what makes the decoder-confusion event (S5b) achievable at the Wyner–Ziv rate. Mirror of Slepian–Wolf swJointTypicalDecoder.

If the covering codeword c₁.decoder m₁ is jointly typical with y and is the unique bin-f m₁ codebook member so typical, then wzBinTypicalDecoder recovers it. Mirror of swJointTypicalDecoder_eq_of_unique.

Covering-failure exponent. The codebook-averaged probability that a strongly-typical source x finds no covering codeword jointly typical with it decays doubly-exponentially: ∫ x, (1 − p_typ x)^{M₁} ≤ exp(−M₁ · exp(−n(I + δ))), where p_typ x is the per-codeword conditional-typicality mass (bounded below by exp(−n(I + δ)) via wz_covering_sideInfo_mass_ge), passed here as hmass.

hmass is the per-source covering-acceptance mass lower bound exp(−n(I+δ)) ≤ p_typ x. With it, (1−p)^M₁ ≤ e^{−M₁ p} ≤ e^{−M₁·exp(−n(I+δ))} pointwise (p_typ x ∈ [0,1], p ≥ exp(−n(I+δ))), then integrate over the probability measure P_X. The pointwise p_typ x ≤ 1 holds even without measurability of Us 0: μ.map (Us 0) is a sub-probability measure (Measure.isFiniteMeasure_map + map mass ≤ 1), so its product Measure.pi is a sub-probability measure (Measure.pi_univ), and the mass of any set is ≤ 1. The (1−t)^M ≤ e^{−Mt} step reuses one_sub_pow_le_exp_neg_mul. @audit:ok

Codebook-restricted decoder confusion exponent. The binning-averaged probability that some codebook member c₁.decoder m' other than the true covering codeword shares the true bin and is jointly typical with Y^n is at most M₁ · exp(−n · I(U;Y)) · M⁻¹.

Restricting the confusable set to the covering codebook is what achieves the Wyner–Ziv rate. Binning all u-sequences would give the count exp(n·H(U|Y)), forcing the rate down to H(U|Y) — too weak; this bound instead restricts to the covering codebook (M₁ = ⌈exp(n·I(X;U))⌉ members), so the alias count is M₁ rather than exp(n·H(U|Y)). With M = ⌈exp(n·R)⌉ bins, the bound is M₁ · exp(−n·I(U;Y)) / M ≈ exp(n·(I(X;U) − I(U;Y) − R)), which vanishes precisely when R > I(X;U) − I(Y;U) — the Wyner–Ziv rate.

hmass is the per-codeword joint-typicality mass upper bound μ{codeword m' typical with Y^n} ≤ exp(−n·I_YU) (the AEP bound for a covering codeword independent of Y^n); hcollision is the binning-collision property binMeas{f | f m' = f m} = M⁻¹ for distinct indices, mirroring binning_collision_prob. The codebook-restricted union over m' : Fin M₁ stays in the body (not a hypothesis): swap the order of integration, bound the per-ω binMeas-slice by union bound + hcollision as M⁻¹ · #{m' typical}, integrate over μ, then apply hmass to each of the M₁ codewords to get M⁻¹ · M₁ · exp(−n·I_YU). hYs/htrueIdx (measurability of the side-information block RV and of the covering index) are regularity preconditions for the Tonelli swap, supplied by the call site.

Implementation note: the typical set is an abstract measurable set jts (parameter hjts_meas : MeasurableSet jts) rather than a concrete jointlyTypicalSet, since the body uses no property of it beyond measurability. This lets the call site instantiate the confusion integral under the source product measure with the typical set defined on the side-information ambient — two different measures a concrete typical set could never match; the per-codeword mass hmass is then supplied via a side-information-marginal transfer to wz_covering_codeword_sideInfo_mass_le. @audit:ok

Source-extension lift α' → α. Lift a Wyner–Ziv code over the source support subtype α' := {x // 0 < P_X x} to a code over the full alphabet α, using the default support element x₀ for out-of-support coordinates (which have zero Measure.pi P_XY-mass, so the lift preserves expected block distortion via wz_expectedBlockDistortion_source_agree). The decoder is unchanged (it does not touch α). Pure def.

Index-binning measure. Hash each of the M₁ covering-codebook indices Fin M₁ independently to a uniformly random bin in Fin M. This is the Fin M₁-index analogue of binningMeasure (which hashes whole sequences (Fin n → α) → Fin M); it is the concrete binMeas : Measure (Fin M₁ → Fin M) that the codebook-restricted decoder-confusion exponent wz_codebook_confusion_expectation_le consumes.

The index-binning measure is a probability measure.

Singleton mass for the index-binning measure. For any hash function f : Fin M₁ → Fin M, its wzIndexBinningMeasure-mass is (1/M)^{M₁} (each of the M₁ covering indices independently picks one of M bins). The Fin M₁-index mirror of binningMeasure_singleton_real.

Index-binning collision probability. Two distinct covering indices m' ≠ m hash to the same bin with probability exactly 1/M. Supplies hcollision to wz_codebook_confusion_expectation_le; the Fin M₁-index mirror of binning_collision_prob.

Mutual-information restriction identity. The covering mutual information computed on the support-restricted joint qStar (over the source support subtype α' := {x // 0 < P_X x}) equals the Wyner–Ziv covering objective wzMutualInfoXU computed on the full-alphabet factorizable joint q'. The support restriction drops only zero atoms of the source marginal P_X, which contribute Real.negMulLog 0 = 0 to every marginal and joint entropy sum, so the two mutual informations coincide. This algebraic leaf lets the covering family hcov — whose premise is mutualInfoPmf qStar < R₁ — be fed at a covering rate R₁ chosen strictly above wzMutualInfoXU q' = I(X;U).

The support-restriction principle (key) sums the vanishing off-support terms away (Real.negMulLog 0 = 0), matching the three marginal/joint entropy sums of qStar (over the support subtype) against those of wzMarginalXU q' (over the full alphabet). The factorization hypotheses hfact_eq/hκ'sum/hqStar_eq are genuine definitional constraints (without them the two mutual informations differ, since qStar lives over the support subtype and q' over the full alphabet); none is the conclusion. @audit:ok

Covering-codeword side-information mass upper bound. For any fixed covering codeword u : Fin n → Fin k, the probability (over the noise generating Y^n = jointRV Ys n) that u is jointly typical with Y^n is at most exp(−n · I_YU), where I_YU ≲ I(U;Y). This is the per-codeword AEP mass bound that wz_codebook_confusion_expectation_le consumes as its hmass hypothesis: because the covering codewords are drawn independently of the side information Y, a fixed covering codeword lands in a Y^n-conditional typical slice with the packing exponent exp(−n · I(U;Y)).

The per-codeword form is assembled directly from single-symbol pmf products (no joint-sequence independence is needed and none is available in the hypotheses). Reframing the ω-event as the Y-law mass of the fixed-u slice {y | (u, y) ∈ jointlyTypicalSet} (via map_measureReal_apply on jointRV Ys n), the slice mass is bounded by ∑_{y} exp(−n(H(Y)−ε)) · [1 ≤ exp(n(H(Z)+ε))·∏ P_Z(u,y)]; folding in the joint-typical product lower bound (prod_map_singleton_ge_of_mem_typicalSet) and marginalizing ∑_y ∏_i P_Z(u_i,y_i) = ∏_i P_U(u_i) (Finset.prod_univ_sum + sum_real_prod_singleton_of_map_fst_eq), the U-typical product bound (prod_map_singleton_le_of_mem_typicalSet) gives mass ≤ exp(−n(H(U)+H(Y)−H(U,Y)−3ε)) = exp(−n(I(U;Y)−3ε)) ≤ exp(−n·I_YU) since hI_YU : I_YU ≤ I(U;Y) − 3ε. For an atypical u the slice is empty and the mass is 0.

The exponent slack 3ε is exactly the sum of the joint-product slack (ε) and the Y/U typicality slacks (ε each); hI_YU is a precondition supplying the standard typicality slack, not load-bearing (the upper bound on I_YU only weakens the RHS exp(−n·I_YU)). hindepU/hidentU/hε are inherited regularity preconditions that the pmf-side assembly does not consume. @audit:ok