Total polynomial-time initialization of the numerical block schedule

Choose L=clog 2 (n+1), clip depth to min requested L, and set the local error exponent to e+depth+2. The independent bound 4^depth ≤ 4*(n+1)^2 permits bounded-power construction of the initial entropy. The actual initial compressed width can then be computed without using a circular capacity assumption.

Every initializer parameter has a uniform unary certificate on all natural inputs. The selected reserve automatically satisfies the finite capacity and splitting budgets. These arithmetic choices instantiate the previously proved finite schedule; the payload evaluator and final statistical specialization are separate layers.

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

Depth clipping bounds the variable power directly by the original input length.

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

The selected initial compressed width contains the entropy and has bounded expansion.

theorem Algebraic.Cutwidth.Extractor.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

The total parameter choice supplies the global reserve premise of the finite schedule.

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

The input logarithm is uniformly polynomial-time in unary.

theorem Algebraic.Cutwidth.Extractor.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)

Clipping a runtime requested depth is uniformly polynomial-time.

theorem Algebraic.Cutwidth.Extractor.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)

Compute the local error exponent from the clipped depth and requested error.

theorem Algebraic.Cutwidth.Extractor.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)

The selected leaf reserve has a uniform unary certificate.

theorem Algebraic.Cutwidth.Extractor.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)

Construct initial entropy using a power bounded independently by the original input.

theorem Algebraic.Cutwidth.Extractor.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)

The actual initial compressed width is uniformly polynomial-time in all runtime inputs.

theorem Algebraic.Cutwidth.Extractor.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

Initialize the encoded numerical state uniformly, with no validity premise on the inputs.

theorem Algebraic.Cutwidth.Extractor.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

Uniformly run the initialized numerical state up to a runtime requested level, clipped to the scheduled depth so that every intermediate state has its proved bound.