Per-covering-codeword side-information typicality mass, under the source product measure. For any fixed covering codeword u : Fin n → Fin k, the probability — under the Wyner–Ziv source product measure Measure.pi of p ↦ P_XY{(p.1.1, p.2)} on α' × β — that u is jointly typical (radius ε, side-information ambient rdAmbient (wzSideInfoMarginal P_XY κ')) with the side-information block fun i ↦ (p i).2 is at most exp(−n · (I(Y;U) − 3ε)), where I(Y;U) = wzMutualInfoYU (Fin k) q'.

This transports wz_covering_codeword_sideInfo_mass_le from the side-information ambient onto the source product measure. Two facts do the work. Side-information-law agreement: the source pair law's β-marginal is y ↦ ∑_x P_XY{(x,y)}, and the β-coerced β'-marginal of wzSideInfoMarginal summed over the covering codeword is y ↦ ∑_x κ' x u · P_XY{(x,y)} = ∑_x P_XY{(x,y)} by hκ'sum, so the source's n-fold Y-law is the β-image (Subtype.val) of the ambient's β'-Y-law (Measure.pi_map_pi + the iid n-fold law) and the fixed-u slice mass is preserved (the β-vs-β' alphabet gap is absorbed by the injective coercion, under which entropy and pmfLog are invariant). Exponent bridge: wzMutualInfoYU (Fin k) q' equals the ambient's I(U;Y) = H(U)+H(Y)-H(U,Y) (the β-values outside β' carry zero mass, negMulLog 0 = 0), which discharges the exponent hypothesis at I_YU := wzMutualInfoYU q' - 3ε.

Non-bundled: the conclusion is a per-codeword mass upper bound (Measure.real {…} ≤ exp …), not the operational error probability; hκ'pos/hκ'sum/hfact_eq are the covering-kernel regularity preconditions, and the exponent is pinned to the actual pmf by hfact_eq (no free-exponent gap).

@audit:ok

Codebook-restricted confusion (E2) probability is squeezable. For a covering codebook of size M₁ ≲ exp(n·R₁) and n beyond a threshold, at the shared conditional-typicality radius ε (an explicit input, pinned to the covering-acceptance mass precondition and used as the bin-decoder radius) there is a derandomized index binning f making the bin-decoder confusion probability so small that distortionMax dα' · Pr[E2] ≤ δ/4. Combines the binning-averaged confusion exponent (wz_codebook_confusion_expectation_le, fed wz_covering_codeword_sideInfo_mass_le + collision wzIndexBinningMeasure_collision, instantiated over the positive-Y-marginal subtype β'), the binning derandomization, and the exponent squeeze (hε_conf : R₁ − I(Y;U) + 3·ε < R), with the source ↔ side-info-ambient identification.

The full event {bin decoder fails to recover the true covering word} decomposes as E2 ⊆ E2b {some other bin member typical, confusion} ∪ C2 {true word not jointly typical, covering-acceptance failure}. Two hypotheses are therefore load-free preconditions, not the analytic core: the covering codebook size upper bound (M₁ : ℝ) ≤ exp(n·R₁) + 1 (the confusion count scales with the number of codewords, so the E2b squeeze needs M₁ capped near ⌈exp(n·R₁)⌉, the size the covering theorem actually produces), and the pinned covering-acceptance mass hcov_accept (a precondition-exposure of the covering code's own acceptance-mass property, discharged by the covering atom). The radius ε is pinned at a single explicit value; the huge-ε regime that makes wzCoveringAcceptFailSet vacuously empty is excluded by hε_conf (wzCoveringAcceptFailSet's mass is monotone decreasing in ε), and dα' is tied to d by hd'_link : ∀ x' g, dα' x' g = d x'.1 g (so distortionMax dα' ≤ distortionMax d).

The body is sorry-free: it proves {decoder ≠ true word} ⊆ C2 ∪ E2b (wzBinTypicalDecoder_eq_of_unique contrapositive), bounds C2 by the pinned hcov_accept premise, chooses f by one derandomization (exists_le_integral over wzIndexBinningMeasure fed the confusion bound, whose per-codeword mass is wz_source_codeword_sideInfo_mass_le), and squeezes the confusion exponent to 0 (wz_tendsto_exp_mul_codebookSize_inv; the degenerate M₁ ≤ 1 covering has an empty confusion event, handled by Subsingleton (Fin M₁)), then scales by distortionMax dα' ≤ distortionMax d.

Per-n Wyner–Ziv code family at a fixed covering rate. Given the covering data together with an already-chosen covering rate R₁ (strictly above I(X;U), so that hcov₁ — the covering LossyCode family at rate R₁ — is available) and the net-rate gap hsplit : R₁ − I(Y;U) < R, assemble the per-n Wyner–Ziv code family at the operational rate R: bin the covering index down to codebookSize R n messages (wzIndexBinningMeasure), decode by the bin conditional-typicality search (wzCodeOfCoveringBinning / wzBinTypicalDecoder), bound the covering-failure (wz_covering_failure_prob_le, fed the mass lower bound via wz_covering_sideInfo_mass_ge) and the codebook-restricted decoder-confusion ( wz_codebook_confusion_expectation_le, fed the per-codeword mass upper bound via wz_covering_codeword_sideInfo_mass_le and the collision wzIndexBinningMeasure_collision) error events, extract a good deterministic codebook + binning by double derandomization, squeeze the residual distortion excess to 0, and extend the covering code α' → α (wzLiftSupportCode).

No error-probability or decoder-correctness claim is a hypothesis: hcov₁ is the separately-established rate-distortion covering LossyCode family at covering rate R₁ (≈ I(X;U)), not the binned WynerZivCode at operational rate R; the index binning, the bin decoder, and the confusion exponent are the residual body work. The distortion budget is split so hfeas/hcov₁ target D + δ/2, reserving δ/2 for the finite-n error terms (mirrors the rate-distortion sister rate_distortion_achievability): the WZ distortion decomposes as a good-event proxy + distortionMax d · (P[E1]+P[E2]), so the reserved slack is absorbed by the error exponents (all → 0). Three preconditions are definitional/regularity, not load-bearing on the operational conclusion: hd'_eq pins the covering proxy d' to 𝔼_{Y|X}[d ∘ qf.2] (killing the d' := 0 counterexample, where the real WZ distortion under d ∘ qf.2 would be unconstrained), hqf supplies the test channel's WynerZivFactorizableConstraint membership (the Markov U-X-Y structure), and hcov₁ exposes the covering size bounds ⌈exp(n·R₁)⌉ ≤ M ≤ exp(n·R₁) + 1 (the E2 squeeze needs M capped above, the ceiling size the covering theorem actually produces). All are discharged by construction at wz_coveringFamily_of_testChannel. hobj'/hsplit/hfeas are objective/feasibility/rate preconditions; positivity and simplex membership are regularity.