Uniform bounded evaluation of the numerical block schedule

The two-component numerical transition agrees with the prescribed width and entropy through the scheduled depth. Its string evaluator has one uniform polynomial-time certificate. Complete iteration additionally bounds every state, including the fixed error workspace; the proved schedule bounds supply a width of 6*initial+E+6 bits.

These are arithmetic and machine consequences for the finite recursive program. Its probabilistic source credits are in Recursion.Extraction. The statements here compute numerical parameters; evaluating the block payload and consuming its seeds are separate constructions.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockStateStep_iterate (initial h Q E : ℕ) {i : ℕ} (level : i ≤ h) : (scheduledBlockStateStep E)^[i] (initial, recursiveBlockEntropy h Q 0) = (recursiveBlockWidth initial h Q E i, recursiveBlockEntropy h Q i)

Division by four tracks the prescribed entropy at every executed level.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockStateStepEval_encode (E : ℕ) (state : ℕ × ℕ) : scheduledBlockStateStepEval (encodeScheduledBlockState E state) = encodeScheduledBlockState E (scheduledBlockStateStep E state)

The total string step computes the numerical transition on encoded states.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockStateStepEval_iterate (E : ℕ) (state : ℕ × ℕ) (i : ℕ) : scheduledBlockStateStepEval^[i] (encodeScheduledBlockState E state) = encodeScheduledBlockState E ((scheduledBlockStateStep E)^[i] state)

Repeated string steps compute the exact numerical iterate.

theorem Algebraic.Cutwidth.Extractor.encodeScheduledBlockState_length (E : ℕ) (state : ℕ × ℕ) : (encodeScheduledBlockState E state).length = 4 * state.1 + 2 * state.2 + E + 6

Exact unary state width, including both pairing separators and fixed workspace.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockStateStepEval_mem_FP : scheduledBlockStateStepEval ∈ Complexity.FP

One numerical state transition is uniformly polynomial-time on every input word.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockState_iterate_mem_FP {initial entropy E count B : List Bool → ℕ} (hinitial : Complexity.UnaryFn initial) (hentropy : Complexity.UnaryFn entropy) (hE : Complexity.UnaryFn E) (hcount : Complexity.UnaryFn count) (hB : Complexity.UnaryFn B) (bounded : ∀ (z : List Bool), ∀ j ≤ count z, ((scheduledBlockStateStep (E z))^[j] (initial z, entropy z)).1 ≤ B z ∧ ((scheduledBlockStateStep (E z))^[j] (initial z, entropy z)).2 ≤ B z) : (fun (z : List Bool) => encodeScheduledBlockState (E z) ((scheduledBlockStateStep (E z))^[count z] (initial z, entropy z))) ∈ Complexity.FP

Complete numerical iteration is polynomial-time under a bound on every intermediate state.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockState_mem_FP {initial h Q E count : List Bool → ℕ} (hinitial : Complexity.UnaryFn initial) (hentropy : Complexity.UnaryFn fun (z : List Bool) => recursiveBlockEntropy (h z) (Q z) 0) (hE : Complexity.UnaryFn E) (hcount : Complexity.UnaryFn count) (capacity : ∀ (z : List Bool), recursiveBlockEntropy (h z) (Q z) 0 ≤ initial z) (budget : ∀ (z : List Bool), 3 * (24 * explicitCondenserBudget (initial z) (recursiveBlockEntropy (h z) (Q z) 0) (E z)) + 6 * E z ≤ 2 * Q z) (levels : ∀ (z : List Bool), count z ≤ h z) : (fun (z : List Bool) => encodeScheduledBlockState (E z) (recursiveBlockWidth (initial z) (h z) (Q z) (E z) (count z), recursiveBlockEntropy (h z) (Q z) (count z))) ∈ Complexity.FP

The global reserve and capacity bounds certify every intermediate scheduled state.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockEntropy_zero_unaryFn {initial h Q : List Bool → ℕ} (hinitial : Complexity.UnaryFn initial) (hh : Complexity.UnaryFn h) (hQ : Complexity.UnaryFn Q) (capacity : ∀ (z : List Bool), recursiveBlockEntropy (h z) (Q z) 0 ≤ initial z) : Complexity.UnaryFn fun (z : List Bool) => recursiveBlockEntropy (h z) (Q z) 0

A certified capacity bound permits uniform unary generation of the initial entropy. The bounded-power computation also handles a zero leaf reserve.