Greedy core (node 1.2.1; 05_prerounding.tex, lem greedy-core).
With θ = P(W_[n]) > 0, 0 < δ < 1, and log(1/θ)/δ < n, there is a
proper subset D ⊊ [n] with |D| ≤ log(1/θ)/δ, P(W_D) ≥ θ, and
average conditional success (1/(n−|D|)) ∑_{i∉D} P(W_i | W_D) ≥ 1 − δ.
All conditionals are defined because W_[n] ⊆ W_D gives
P(W_D) ≥ θ > 0.
Core parameters and bounds (node 1.2.2; 05_prerounding.tex, eqs
p-q-m, eta-definition, core-basic-bounds, eta-gamma-bound). With
δ = ε/4, m = n − |D|, p = P(W_D) ∈ [θ, 1], t₀ = log(1/p),
s₀ = |D|·ℓ, η = (t₀ + s₀)/m, the pre-rounding hypotheses
θ > e^{−γn}, 0 < ε ≤ 1, γ ≤ ε/8 give
|D| < 4γn/ε ≤ n/2 (so m > n/2), t₀ < γn, and
η < 2γ(1 + 4ℓ/ε) ≤ 8γ(ε + ℓ)/ε. The q ≥ 1 − ε/4 part of eq
core-basic-bounds is not restated here: it is verbatim the third conjunct
of greedy_core at δ = ε/4 (node 1.2.2 lists it as a "put" item) and
is consumed directly from there.