Uniform bounded evaluation of all internal block levels

The actual block payload and seed-consumption loop is polynomial-time uniformly in its unary parameters and input words, provided the supplied entropy schedule satisfies the proved global reserve budget and has a positive leaf reserve. Every intermediate encoding is bounded by eighteen times the initial compressed width, twice the error exponent, the original seed-word length, and a constant.

The proof certifies the complete iteration, including all numerical values, block counts, payloads, and unused seeds. The exact statistical meaning of canonical seed words and the final leaf extraction are separate layers.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockRunStepEval_encode (E : ℕ) (state : ScheduledBlockRunState) : scheduledBlockRunStepEval (encodeScheduledBlockRun E state) = encodeScheduledBlockRun E (scheduledBlockRunStep E state)

The encoded runtime step computes the structured block and seed update.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockRunStepEval_iterate (E : ℕ) (state : ScheduledBlockRunState) (i : ℕ) : scheduledBlockRunStepEval^[i] (encodeScheduledBlockRun E state) = encodeScheduledBlockRun E ((scheduledBlockRunStep E)^[i] state)

Any finite encoded run agrees with the structured iteration.

theorem Algebraic.Cutwidth.Extractor.encodeScheduledBlockRun_length (E : ℕ) (state : ScheduledBlockRunState) : (encodeScheduledBlockRun E state).length = 8 * state.dimensions.1 + 4 * state.dimensions.2 + 2 * E + 2 * state.count + 2 * state.payload.length + state.seeds.length + 18

Exact storage cost of the runtime block-state encoding.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockRun_dimensions (n h Q E : ℕ) (source seeds : List Bool) : (scheduledBlockRun n h Q E source seeds).dimensions = (recursiveBlockWidth (scheduledBlockInitialWidth n h Q E) h Q E h, Q)

The actual loop finishes at the scheduled leaf width and leaf entropy reserve.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockRun_count (n h Q E : ℕ) (source seeds : List Bool) : (scheduledBlockRun n h Q E source seeds).count = 2 ^ h

Each requested level doubles the number of blocks, independently of their contents.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockRun_iterate_bound (n h Q E : ℕ) (source seeds : List Bool) (positive : 0 < Q) (budget : 3 * (24 * explicitCondenserBudget (scheduledBlockInitialWidth n h Q E) (recursiveBlockEntropy h Q 0) E) + 6 * E ≤ 2 * Q) {i : ℕ} (level : i ≤ h) : (encodeScheduledBlockRun E ((scheduledBlockRunStep E)^[i] (scheduledBlockRunInitial n h Q E source seeds))).length ≤ 18 * scheduledBlockInitialWidth n h Q E + 2 * E + seeds.length + 18

The finite schedule bounds every complete intermediate block-state encoding.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockRunStepEval_mem_FP : scheduledBlockRunStepEval ∈ Complexity.FP

The total encoded step is polynomial-time on every input string.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockRun_mem_FP {n h Q E : List Bool → ℕ} {source seeds : List Bool → List Bool} (hn : Complexity.UnaryFn n) (hentropy : Complexity.UnaryFn fun (z : List Bool) => recursiveBlockEntropy (h z) (Q z) 0) (hh : Complexity.UnaryFn h) (hE : Complexity.UnaryFn E) (hsource : source ∈ Complexity.FP) (hseeds : seeds ∈ Complexity.FP) (positive : ∀ (z : List Bool), 0 < Q z) (budget : ∀ (z : List Bool), 3 * (24 * explicitCondenserBudget (scheduledBlockInitialWidth (n z) (h z) (Q z) (E z)) (recursiveBlockEntropy (h z) (Q z) 0) (E z)) + 6 * E z ≤ 2 * Q z) : (fun (z : List Bool) => encodeScheduledBlockRun (E z) (scheduledBlockRun (n z) (h z) (Q z) (E z) (source z) (seeds z))) ∈ Complexity.FP

One uniform polynomial-time program evaluates the initial condenser and all internal levels, with an explicit bound throughout the run.