Instantiating the near-halving recursive extraction guarantee

The identity supplies the initial one-block source, and the actual paired condensers satisfy the generic recursion's two entropy inequalities. The leaf gap pays the final one-shot threshold. The existing dyadic error sum retains all shared seeds and bounds the whole recursive program.

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockExtractor_weighted [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] (n h Q E : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ n) (budget : 12 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget n (nearHalvingBlockEntropy h Q 0) E + 4 * E ≤ Q) : WeightedStrongSeededExtractor (nearHalvingBlockExtractor n h Q E) (2 ^ nearHalvingBlockEntropy h Q 0) ((3 * 2 ^ h - 1) * (2 ^ E)⁻¹)

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockExtractor_dyadic [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] (n h Q e : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ n) (budget : 12 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget n (nearHalvingBlockEntropy h Q 0) (e + h + 2) + 4 * (e + h + 2) ≤ Q) : WeightedStrongSeededExtractor (nearHalvingBlockExtractor n h Q (e + h + 2)) (2 ^ nearHalvingBlockEntropy h Q 0) (2 ^ e)⁻¹