Bounds for the constant-rate block schedule

Monotonicity of the logarithmic budget bounds every field seed using the initial parameters. The leaf reserve then pays the split budget at every executed level, and induction controls the actual rounded block widths.

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockEntropy_last (h Q : ℕ) : recursiveBlockEntropy h Q h = Q

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockEntropy_succ (h Q : ℕ) {i : ℕ} (level : i < h) : recursiveBlockEntropy h Q i = 4 * recursiveBlockEntropy h Q (i + 1)

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockEntropy_reserve_le (h Q i : ℕ) : Q ≤ recursiveBlockEntropy h Q i

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockEntropy_le_initial (h Q i : ℕ) : recursiveBlockEntropy h Q i ≤ recursiveBlockEntropy h Q 0

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenserBudget_mono {n k n' k' E : ℕ} (width : n ≤ n') (entropy : k ≤ k') : explicitCondenserBudget n k E ≤ explicitCondenserBudget n' k' E

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockSeedWidth_le_of_width (initial h Q E i : ℕ) (width : recursiveBlockWidth initial h Q E i ≤ initial) : recursiveBlockSeedWidth initial h Q E i ≤ 24 * explicitCondenserBudget initial (recursiveBlockEntropy h Q 0) E

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlock_step (initial h Q E : ℕ) (budget : 3 * (24 * explicitCondenserBudget initial (recursiveBlockEntropy h Q 0) E) + 6 * E ≤ 2 * Q) {i : ℕ} (level : i < h) (width : recursiveBlockWidth initial h Q E i ≤ initial) : recursiveBlockEntropy h Q (i + 1) ≤ recursiveBlockWidth initial h Q E (i + 1) ∧ recursiveBlockWidth initial h Q E (i + 1) + recursiveBlockEntropy h Q (i + 1) + E ≤ recursiveBlockEntropy h Q i

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockWidth_bounds (initial h Q E : ℕ) (capacity : recursiveBlockEntropy h Q 0 ≤ initial) (budget : 3 * (24 * explicitCondenserBudget initial (recursiveBlockEntropy h Q 0) E) + 6 * E ≤ 2 * Q) {i : ℕ} (level : i ≤ h) : recursiveBlockEntropy h Q i ≤ recursiveBlockWidth initial h Q E i ∧ recursiveBlockWidth initial h Q E i ≤ initial

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlock_split_budget (initial h Q E : ℕ) (capacity : recursiveBlockEntropy h Q 0 ≤ initial) (budget : 3 * (24 * explicitCondenserBudget initial (recursiveBlockEntropy h Q 0) E) + 6 * E ≤ 2 * Q) {i : ℕ} (level : i < h) : recursiveBlockEntropy h Q (i + 1) ≤ recursiveBlockWidth initial h Q E (i + 1) ∧ recursiveBlockWidth initial h Q E (i + 1) + recursiveBlockEntropy h Q (i + 1) + E ≤ recursiveBlockEntropy h Q i

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockSeedWidth_le (initial h Q E : ℕ) (capacity : recursiveBlockEntropy h Q 0 ≤ initial) (budget : 3 * (24 * explicitCondenserBudget initial (recursiveBlockEntropy h Q 0) E) + 6 * E ≤ 2 * Q) {i : ℕ} (level : i ≤ h) : recursiveBlockSeedWidth initial h Q E i ≤ 24 * explicitCondenserBudget initial (recursiveBlockEntropy h Q 0) E

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlock_entropy_mass_le (h Q : ℕ) {i : ℕ} (level : i ≤ h) : 2 ^ i * recursiveBlockEntropy h Q i ≤ recursiveBlockEntropy h Q 0

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlock_payload_le (initial h Q E : ℕ) (capacity : recursiveBlockEntropy h Q 0 ≤ initial) (budget : 3 * (24 * explicitCondenserBudget initial (recursiveBlockEntropy h Q 0) E) + 6 * E ≤ 2 * Q) {i : ℕ} (level : i ≤ h) : 2 ^ i * recursiveBlockWidth initial h Q E i ≤ 2 * initial

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlock_count_le (h Q : ℕ) {i : ℕ} (positive : 0 < Q) (level : i ≤ h) : 2 ^ i ≤ recursiveBlockEntropy h Q 0