Total initialization with an independent bounded power

Clipping depth to the ceiling input logarithm bounds its fourth power by 4*(n+1)^2. This original-input bound certifies the initial entropy before constructing the compressed width, avoiding a circular capacity argument. The existing finite reserve theorems then supply all schedule premises.

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockDepth_pow_four_le (n requested : ℕ) : 4 ^ scheduledBlockDepth n requested ≤ 4 * (n + 1) ^ 2

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockRuntimeInitialWidth_bounds (n requested e : ℕ) : scheduledBlockInitialEntropy n requested e ≤ scheduledBlockRuntimeInitialWidth n requested e ∧ scheduledBlockRuntimeInitialWidth n requested e ≤ 64 * scheduledBlockInitialEntropy n requested e

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockRuntime_reserve_budget (n requested e : ℕ) : 3 * (24 * explicitCondenserBudget (scheduledBlockRuntimeInitialWidth n requested e) (scheduledBlockInitialEntropy n requested e) (scheduledBlockErrorExponent n requested e)) + 6 * scheduledBlockErrorExponent n requested e ≤ 2 * scheduledBlockLeafReserve n requested e

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockInputLog_unaryFn {n : List Bool → ℕ} (hn : Complexity.UnaryFn n) : Complexity.UnaryFn fun (z : List Bool) => scheduledBlockInputLog (n z)

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockDepth_unaryFn {n requested : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hrequested : Complexity.UnaryFn requested) : Complexity.UnaryFn fun (z : List Bool) => scheduledBlockDepth (n z) (requested z)

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockErrorExponent_unaryFn {n requested e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hrequested : Complexity.UnaryFn requested) (he : Complexity.UnaryFn e) : Complexity.UnaryFn fun (z : List Bool) => scheduledBlockErrorExponent (n z) (requested z) (e z)

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockLeafReserve_unaryFn {n requested e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hrequested : Complexity.UnaryFn requested) (he : Complexity.UnaryFn e) : Complexity.UnaryFn fun (z : List Bool) => scheduledBlockLeafReserve (n z) (requested z) (e z)

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockInitialEntropy_unaryFn {n requested e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hrequested : Complexity.UnaryFn requested) (he : Complexity.UnaryFn e) : Complexity.UnaryFn fun (z : List Bool) => scheduledBlockInitialEntropy (n z) (requested z) (e z)

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockRuntimeInitialWidth_unaryFn {n requested e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hrequested : Complexity.UnaryFn requested) (he : Complexity.UnaryFn e) : Complexity.UnaryFn fun (z : List Bool) => scheduledBlockRuntimeInitialWidth (n z) (requested z) (e z)

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockStateInit_mem_FP {n requested e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hrequested : Complexity.UnaryFn requested) (he : Complexity.UnaryFn e) : (fun (z : List Bool) => scheduledBlockStateInit (n z) (requested z) (e z)) ∈ Complexity.FP

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockStateInit_iterate_mem_FP {n requested e count : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hrequested : Complexity.UnaryFn requested) (he : Complexity.UnaryFn e) (hcount : Complexity.UnaryFn count) : (fun (z : List Bool) => scheduledBlockStateStepEval^[min (count z) (scheduledBlockDepth (n z) (requested z))] (scheduledBlockStateInit (n z) (requested z) (e z))) ∈ Complexity.FP