Exact and bounded evaluation of the near-halving payload loop

The encoded step follows the structured state on every canonical encoding. Its numeric fields follow the actual rounded width schedule, while its payload has fixed block width after each positive number of steps. Bounds include static parameters, block counts, the arbitrary initial payload, and the unused seed suffix. Zero-step runs require no entropy or reserve premise.

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

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

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

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockRunStep_iterate_count (h Q E : ℕ) (state : NearHalvingBlockRunState) (i : ℕ) : ((nearHalvingBlockRunStep h Q E)^[i] state).count = 2 ^ i * state.count

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

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockRunStep_iterate_seeds_length (h Q E : ℕ) (state : NearHalvingBlockRunState) (i : ℕ) : ((nearHalvingBlockRunStep h Q E)^[i] state).seeds.length ≤ state.seeds.length

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

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockRunStep_iterate_payload_length (h Q E : ℕ) (state : NearHalvingBlockRunState) {i : ℕ} (positive : 0 < i) : ((nearHalvingBlockRunStep h Q E)^[i] state).payload.length = ((nearHalvingBlockRunStep h Q E)^[i] state).count * ((nearHalvingBlockRunStep h Q E)^[i] state).width

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

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

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

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