Reserve estimates for the constant-rate recursive schedule #
The initial rate-one compression has width comparable to the initial entropy. Taking logarithms of that bound controls every later condenser budget by the depth and the logarithm of the leaf reserve. These are finite arithmetic estimates, independent of the recurrence induction and of runtime claims.
theorem
Algebraic.Cutwidth.Extractor.Internal.recursiveBlockInitialWidth_bounds
(n L E h : ℕ)
(length : Nat.clog 2 (n + 1) ≤ L)
:
have Q := recursiveBlockReserve L E;
have k := recursiveBlockEntropy h Q 0;
have N := explicitCondenserHalfWidth n k E 1 + explicitCondenserHalfWidth n k E 1;
k ≤ N ∧ N ≤ 64 * k
theorem
Algebraic.Cutwidth.Extractor.Internal.recursiveBlockInitialBudget_le
(n L E h : ℕ)
(length : Nat.clog 2 (n + 1) ≤ L)
:
have Q := recursiveBlockReserve L E;
have k := recursiveBlockEntropy h Q 0;
have N := explicitCondenserHalfWidth n k E 1 + explicitCondenserHalfWidth n k E 1;
explicitCondenserBudget N k E ≤ E + 4 * h + 2 * Nat.clog 2 (L + E + 1) + 64
theorem
Algebraic.Cutwidth.Extractor.Internal.recursiveBlockReserve_budget
(n L E h : ℕ)
(length : Nat.clog 2 (n + 1) ≤ L)
(depth : h ≤ L)
:
have Q := recursiveBlockReserve L E;
have k := recursiveBlockEntropy h Q 0;
have N := explicitCondenserHalfWidth n k E 1 + explicitCondenserHalfWidth n k E 1;
3 * (24 * explicitCondenserBudget N k E) + 6 * E ≤ 2 * Q