Per-codeword power-constraint expurgation bound.

For a codebook drawn from the 2-stage Gaussian product law at codeword variance P_cb, and a power target P_target with strict slack P_cb < P_target, each individual codeword m violates the power budget ∑ᵢ (c m i)² > n · P_target on a codebook set of mass ≤ ε (for all n past a threshold N₀).

This is the per-codeword marginal form: unlike the false ∀ m-form (mass of the all-codewords-OK set ≥ 1 − ε, which decays like q^M ≈ exp(−exp(n(R−ψ)))), the per-codeword marginal mass is M-independent (the m-th coordinate marginal of Measure.pi (fun _ : Fin M => νₙ) is νₙ), so no exponential rate / capacity rate bound is needed. It is exactly the WLLN/Markov fact the Cover–Thomas expurgation argument consumes.

Proof: the m-th coordinate marginal is νₙ = Measure.pi (fun _ : Fin n => gaussianReal 0 P_cb.toNNReal) (measurePreserving_eval), reducing the codebook mass to the single-codeword chi-square upper-tail mass. Apply the abstract Chebyshev engine pi_empirical_mean_concentration with statistic φ x = x², μ[φ] = (P_cb.toNNReal : ℝ) (centred Gaussian second moment = variance), and the deviation level δ = P_target − (P_cb.toNNReal : ℝ) > 0: the violating set {x | n·P_target < ∑ᵢ xᵢ²} is contained in the deviation set {x | δ ≤ |(∑ᵢ φ(xᵢ))/n − μ[φ]|}, whose mass is ≤ variance(φ)/(n·δ²); choosing N₀ > variance(φ)/(ε·δ²) gives ≤ ε. MemLp φ 2 holds because the Gaussian has a finite 4th moment (memLp_id_gaussianReal 4, polynomial — no log).