Uniform bounded evaluation of the near-halving payload loop

The actual encoded loop follows the specified rounded widths and consumes exactly one shared field seed per level. Every positive iteration count produces a payload of the exact scheduled block length, even from an arbitrary source word. The state-size bound also includes that initial word, all unary workspace, block counts, and unused seeds.

One FP program evaluates any partial run whose requested count is at most the depth and is either zero or has the proved entropy and reserve budgets. The initialization power has its own explicit unary-computation premise; the step updates it by division. Canonical seed semantics and the final one-shot stage are separate layers. This loop uses the finite arithmetic schedule credited in NearHalving.Parameters.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRunStepEval_encode (h Q E : ℕ) (state : NearHalvingBlockRunState) : nearHalvingBlockRunStepEval (encodeNearHalvingBlockRun h Q E state) = encodeNearHalvingBlockRun h Q E (nearHalvingBlockRunStep h Q E state)

The encoded runtime step computes the complete structured workspace update.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRunStepEval_iterate (h Q E : ℕ) (state : NearHalvingBlockRunState) (i : ℕ) : nearHalvingBlockRunStepEval^[i] (encodeNearHalvingBlockRun h Q E state) = encodeNearHalvingBlockRun h Q E ((nearHalvingBlockRunStep h Q E)^[i] state)

Any finite encoded run agrees with structured payload and seed iteration.

theorem Algebraic.Cutwidth.Extractor.encodeNearHalvingBlockRun_length (h Q E : ℕ) (state : NearHalvingBlockRunState) : (encodeNearHalvingBlockRun h Q E state).length = 8 * state.width + 4 * state.remaining + 4 * state.remainingPower + 2 * state.count + 4 * h + 2 * Q + 2 * E + 2 * state.payload.length + state.seeds.length + 28

Exact encoded storage includes every numeric field, payload, and seed suffix.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRun_numeric (N h Q E : ℕ) (source seeds : List Bool) {i : ℕ} (level : i ≤ h) : (nearHalvingBlockRun N h Q E i source seeds).width = nearHalvingBlockWidth N h Q E i ∧ (nearHalvingBlockRun N h Q E i source seeds).remaining = h - i ∧ (nearHalvingBlockRun N h Q E i source seeds).remainingPower = 2 ^ (h - i)

Up to the supplied depth, numeric workspace follows the actual rounded schedule.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRun_succ (N h Q E i : ℕ) (source seeds : List Bool) : nearHalvingBlockRun N h Q E (i + 1) source seeds = nearHalvingBlockRunStep h Q E (nearHalvingBlockRun N h Q E i source seeds)

The next partial run applies one actual payload and seed-consumption step.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRun_count (N h Q E i : ℕ) (source seeds : List Bool) : (nearHalvingBlockRun N h Q E i source seeds).count = 2 ^ i

Every executed step doubles the number of blocks.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRun_seeds (N h Q E : ℕ) (source seeds : List Bool) {i : ℕ} (level : i ≤ h) : (nearHalvingBlockRun N h Q E i source seeds).seeds = List.drop ((Finset.range i).sum (nearHalvingBlockSeedWidth N h Q E)) seeds

The unused suffix drops exactly the sum of the executed field seed widths.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRun_seeds_length (N h Q E i : ℕ) (source seeds : List Bool) : (nearHalvingBlockRun N h Q E i source seeds).seeds.length ≤ seeds.length

The unused seed suffix never exceeds the original seed-word length.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRun_payload_length (N h Q E : ℕ) (source seeds : List Bool) {i : ℕ} (level : i ≤ h) (positive : 0 < i) : (nearHalvingBlockRun N h Q E i source seeds).payload.length = 2 ^ i * nearHalvingBlockWidth N h Q E i

Every positive partial run has exact scheduled payload length, for any initial word.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRun_iterate_bound (N h Q E : ℕ) (source seeds : List Bool) {i : ℕ} (level : i ≤ h) (valid : i = 0 ∨ nearHalvingBlockEntropy h Q 0 ≤ N ∧ 2 * (6 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget N (nearHalvingBlockEntropy h Q 0) E + 2 * E) ≤ Q) : (encodeNearHalvingBlockRun h Q E (nearHalvingBlockRun N h Q E i source seeds)).length ≤ 14 * N + 8 * h + 4 * 2 ^ h + 2 * Q + 2 * E + 2 * source.length + seeds.length + 30

All complete state encodings are bounded; zero steps need no splitting hypotheses.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRunStepEval_mem_FP : nearHalvingBlockRunStepEval ∈ Complexity.FP

The total encoded step is polynomial-time on arbitrary, including malformed, input strings.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockRun_mem_FP {N h Q E count : List Bool → ℕ} {source seeds : List Bool → List Bool} (hN : Complexity.UnaryFn N) (hh : Complexity.UnaryFn h) (hQ : Complexity.UnaryFn Q) (hE : Complexity.UnaryFn E) (hcount : Complexity.UnaryFn count) (hpower : Complexity.UnaryFn fun (z : List Bool) => 2 ^ h z) (hsource : source ∈ Complexity.FP) (hseeds : seeds ∈ Complexity.FP) (levels : ∀ (z : List Bool), count z ≤ h z) (valid : ∀ (z : List Bool), count z = 0 ∨ nearHalvingBlockEntropy (h z) (Q z) 0 ≤ N z ∧ 2 * (6 * (nearHalvingBlockRate (h z) + 1) * explicitCondenserBudget (N z) (nearHalvingBlockEntropy (h z) (Q z) 0) (E z) + 2 * E z) ≤ Q z) : (fun (z : List Bool) => encodeNearHalvingBlockRun (h z) (Q z) (E z) (nearHalvingBlockRun (N z) (h z) (Q z) (E z) (count z) (source z) (seeds z))) ∈ Complexity.FP

One uniform program evaluates the complete payload loop under the explicit state bound. The initialization power is certified separately, and zero steps require no reserve budget.