Matched extraction with a growing recursion depth

The exact scheduled seed estimate fits the existing padded width when the scale pays the displayed depth-error-logarithm product. No upper bound of sixty-four is imposed on the recursion depth. The statistical proof reuses the existing output equivalence and retained-seed padding certificate.

theorem Algebraic.Cutwidth.Extractor.Internal.matchedBlockExtractor_growing_seedBits_le (n h L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (error : e + h + 2 ≤ L) (budget : (h + 1) * (e + 2 * h + Nat.clog 2 (L + 1) + 4) ≤ L) : scheduledBlockSeedBits n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L ≤ matchedBlockSeedBits L

A checked extension of the numerical padded-seed bound to unbounded depth.

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockEntropy_growing_le (h L e : ℕ) (positive : 1 ≤ L) (error : e + h + 2 ≤ L) : recursiveBlockEntropy h (recursiveBlockReserve L (e + h + 2)) 0 ≤ 2 ^ (2 * h + 14) * L

The actual entropy threshold remains quadratic in the requested power-of-two output factor.

theorem Algebraic.Cutwidth.Extractor.Internal.matchedBlockExtractor_growing_weighted (n h L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (error : e + h + 2 ≤ L) (budget : (h + 1) * (e + 2 * h + Nat.clog 2 (L + 1) + 4) ≤ L) : WeightedStrongSeededExtractor (matchedBlockExtractor n h L e) (2 ^ recursiveBlockEntropy h (recursiveBlockReserve L (e + h + 2)) 0) (2 ^ e)⁻¹

The exact scheduled threshold for any depth satisfying the explicit seed budget.

theorem Algebraic.Cutwidth.Extractor.Internal.matchedBlockExtractor_growing (n h L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (error : e + h + 2 ≤ L) (budget : (h + 1) * (e + 2 * h + Nat.clog 2 (L + 1) + 4) ≤ L) : WeightedStrongSeededExtractor (matchedBlockExtractor n h L e) (2 ^ (2 ^ (2 * h + 14) * L)) (2 ^ e)⁻¹

A simple entropy bound for the same actual program at arbitrary depth.

theorem Algebraic.Cutwidth.Extractor.Internal.matchedBlockOutputBits_merging_reserve (t L e : ℕ) (error : e ≤ L) : 2 ^ 62 * L + (2 * t + 2) * matchedBlockSeedBits L + e ≤ matchedBlockOutputBits (Nat.clog 2 (t + 1) + 64) L

A logarithmic depth provides room for middle extraction and all prefix/output leakage.