Computation of the complete near-halving extractor

Compose the certified bounded payload loop with the total final extractor. The iteration certificate accounts for every intermediate state; final field-seed slicing and extraction use registered polynomial-time rules.

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockFinishEval_encode (h Q E ell : ℕ) (state : NearHalvingBlockRunState) : nearHalvingBlockFinishEval (Complexity.pair (encodeNearHalvingBlockRun h Q E state) (List.replicate ell true)) = nearHalvingBlockFinish E ell state

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockFinishEval_mem_FP : nearHalvingBlockFinishEval ∈ Complexity.FP

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockExtractorBits_length (N h Q E ell count : ℕ) (source seeds : List Bool) : (nearHalvingBlockExtractorBits N h Q E ell count source seeds).length = 2 ^ count * ell

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockExtractorBits_mem_FP {N h Q E ell 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) (hell : Complexity.UnaryFn ell) (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) => nearHalvingBlockExtractorBits (N z) (h z) (Q z) (E z) (ell z) (count z) (source z) (seeds z)) ∈ Complexity.FP