If the chosen covering word c.decoder (c.encoder x) typically covers x (covering-success in rdAmbient qStar), then it is U-typical in the side-information ambient. The covering-success U-band bands the word against qStar's U-marginal; L0 makes that identical to the side-information ambient's U-marginal, so the two U-typical sets coincide. Pure set inclusion (no threshold N).

For n large the source-measure mass of the Y-band failure — the side-information block y is not typical in the side-information ambient — is at most tol/4. A one-dimensional AEP on the iid Y-sequence (law P_Y = ∑ₓ P_XY{(x, ·)}), independent of the code c and of covering-success. Transports typicalSet_prob_ge_of_rate (the ℕ-process AEP) onto the source product measure via the β'↔β coercion, mirroring the wz_source_codeword_sideInfo_mass_le transport.

For n large the source-measure mass of the (X,Y)-joint-atypical set — the block (x_i,y_i) = p_i is not typical in the (X,Y)-joint ambient rdAmbient Src (Src(x',y) = P_XY{(x'.1,y)}, the SRC per-coordinate law) — is at most tol/8. The (x_i,y_i) pairs are iid ~ Src under SRC, so this is a direct AEP (typicalSet_prob_ge_of_rate) transported by rdAmbient_map_jointRV_jointSequence_eq_pi. Independent of the code c.

The source-block measure SRC = Measure.pi (fun _ ↦ pmfToMeasure Src) with Src (x, y) = P_XY{(x, y)} disintegrates over the x-block: for any block event S, SRC.real S = ∑_{xb} (∏_i P_X(xb_i)) · condY(xb).real (xb-slice of S), where P_X(x) = ∑_y P_XY{(x, y)} (positive on the x-alphabet subtype) and the conditional y-block measure condY(xb) = Measure.pi (fun i ↦ pmfToMeasure (P(·|xb_i))) uses the normalized per-coordinate law P(y|x) = P_XY{(x, y)} / P_X(x), hence a genuine probability measure — the form the conditional-Chebyshev step consumes. This avoids general condDistrib on Measure.pi (a Mathlib 0-hit); it is elementary finite Fubini via pmfToMeasure atomicity and Measure.pi_pi, with no AEP.

The independent-product mass of the strong joint-typical set under the covering ambient rdAmbient qStar — the probability that an independently drawn covering word U^n is strongly jointly typical with the source block X^n at radius ε — is bounded below by the standard random-coding exponent (1 − η)·exp(n·((H(Z) − H(X) − H(Y)) − slack)). This is the WZ instantiation of jointStronglyTypicalSet_indep_prob_ge, discharging its independence / ident-distribution / full-support / marginal-matching premises from the ambient-regularity lemmas of rdAmbient qStar (full support of qStar gives hposX/Y/Z). It is the covering-success lower bound feeding the joint (distortion + covering-success) derandomize of wz_coveringFamily_of_testChannel.

The radius ε_cov = ε / (2·(1 + C)) at which the covering word is required to be strongly (x, U)-typical, where C = ∑_{x,u} |g(x, u)| is the mean-pin amplification constant of wz_wsm_negLog_mean_pin_of_stronglyTypical (g = wzCondMeanKernel). The mean-pin bounds |M(xb) − H(wsm)| by C · (strong radius), so to keep the conditional-mean statistic within ε/2 of H(wsm) — the slack the correlated Markov core needs to absorb the acceptance-band radius ε — the strong covering radius must be ≤ ε/(2C). Using ε/(2·(1 + C)) makes the choice unconditional (C ≥ 0) and keeps ε_cov > 0. This is a computed term of ε, κ', P_XY (NOT a new lemma parameter), so the chain signatures stay fixed. Strong typicality at the same radius ε would only pin M within C·ε ≫ ε, leaving an O(ε) partial-relabel counterexample class open (a scaled-down label swap); the smaller radius closes that class.

The strong covering radius is positive for ε > 0 (the denominator 2·(1 + ∑|g|) is ≥ 2).

The covering-success event for the strong-Ecov Wyner–Ziv covering chain: the chosen covering word c.decoder (c.encoder x) is jointly typical with the source x in the covering ambient rdAmbient qStar, in BOTH readings.

• The strong reading (jointStronglyTypicalSet) is a per-symbol type pin at the smaller radius wzCoveringStrongRadius P_XY κ' ε = ε/(2(1 + C)); it is the strengthening that makes the correlated Markov core wz_covering_jointBand_markov_core true-as-framed, by pinning the conditional-mean statistic M(xb) to within C · ε_cov < ε/2 of H(wzSideInfoMarginal) through wz_wsm_negLog_mean_pin_of_stronglyTypical. This kills not only the full entropy-preserving label-swap counterexample but the whole O(ε) partial-relabel class that strong typicality at the same radius ε would leave open (there |M − H| ≤ C·ε ≫ ε).
• The weak reading (jointlyTypicalSet) is an entropy band at radius ε; it is retained so that the acceptance-band U-typicality plumbing wz_covering_success_subset_uTypical — which needs the weak U-band at radius ε — goes through unchanged.

Strong typicality at radius ε_cov does not imply the weak U-band at radius ε (the strong-to-weak bridge widens the radius by ε_cov·logSumAbs, an unrelated constant), so the covering-success event is the intersection of the two readings. This keeps every lemma signature in the chain fixed (the radii are computed terms of ε) while making the correlated Markov concentration true-as-framed.

Strong covering-success implies weak covering-success (the second conjunct, at radius ε), the reading the U-typicality plumbing consumes.

For a strong-covering x-block xb — one whose induced (x, U) block (xb i, c.decoder (c.encoder xb) i) is strongly typical for the covering ambient at the strong radius ε_cov = wzCoveringStrongRadius P_XY κ' ε — the conditional side-information measure of the (U, Y)-atypical slice is ≤ tol/8 for n ≥ N. This is the conditional AEP U — X — Y: the mean-pin (wz_wsm_negLog_mean_pin_of_stronglyTypical) puts the conditional mean of -log wsm(U_i, ·) within C·ε_cov < ε/2 of H(wsm), and the conditional Chebyshev (pi_nonuniform_concentration_tendsto, deviation ε/2) concentrates the empirical (U, Y)-entropy there, so (U, Y)-atypicality (radius ε) has vanishing conditional mass. This is the from-scratch conditional-AEP kernel; the surrounding finite-Fubini split, good/bad x-block dichotomy and summation are discharged in wz_covering_jointBand_markov_core.

Implementation notes. The hypothesis uses strong (not weak) typicality: strong typicality pins the per-symbol (x, u)-type in total variation, controlling the linear functional M = ⟨type, g⟩ that the conclusion needs — no finer structure required — whereas weak entropy-only typicality fails on an entropy-preserving label-swap counterexample class. The assembly mirrors the in-tree template wz_covering_yBand_aep: a uniform sup-bound B = ∑_q |log wsm(q)| on the per-coordinate log-statistic, its conditional mean identified with wzCondMeanKernel, and the ambient entropy ∑_q negMulLog(wsm q), combined through the radius-separated mean-pin (C·ε_cov < ε/2) and the Chebyshev engine (pi_nonuniform_concentration_tendsto, δ = ε/2) by a strict triangle inequality. The hκ'_pos/hκ'_sum/hqStar hypotheses are full-support / proper-pmf / qStar–κ' consistency preconditions (used to place qStar ∈ stdSimplex and identify the conditional mean), not the concentration conclusion — not load-bearing; the proof is sorryAx-free.

@audit:ok