Correct and bounded encoded iteration of block payloads

The total encoded step agrees with the structured step. Its numerical projection follows the checked schedule, the count doubles, and the exact output length gives the payload bound even for arbitrary input and seed words. The unused seed suffix can only shrink. Together these facts bound every intermediate encoded state and justify the complete FP iteration.

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockRunStep_iterate_dimensions (E : ℕ) (state : ScheduledBlockRunState) (i : ℕ) : ((scheduledBlockRunStep E)^[i] state).dimensions = (scheduledBlockStateStep E)^[i] state.dimensions

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockRunStep_iterate_count (E : ℕ) (state : ScheduledBlockRunState) (i : ℕ) : ((scheduledBlockRunStep E)^[i] state).count = 2 ^ i * state.count

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockRunStep_iterate_seeds_length (E : ℕ) (state : ScheduledBlockRunState) (i : ℕ) : ((scheduledBlockRunStep E)^[i] state).seeds.length ≤ state.seeds.length

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockRunStep_iterate_payload_length (E : ℕ) (state : ScheduledBlockRunState) (shape : state.payload.length = state.count * state.dimensions.1) (i : ℕ) : ((scheduledBlockRunStep E)^[i] state).payload.length = ((scheduledBlockRunStep E)^[i] state).count * ((scheduledBlockRunStep E)^[i] state).dimensions.1

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockRunInitial_payload_length (n h Q E : ℕ) (source seeds : List Bool) : (scheduledBlockRunInitial n h Q E source seeds).payload.length = scheduledBlockInitialWidth n h Q E

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

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

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

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

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