Uniform evaluation of near-halving recursion and final extraction #
The complete string program emits one fixed-length word per leaf. It is polynomial-time in all runtime parameters under the established intermediate state bound, including an explicit bound for the initial power of two. Zero executed levels need no entropy or reserve hypothesis. The final stage reads only its two exact seed words, allowing unused trailing seed bits.
theorem
Algebraic.Cutwidth.Extractor.nearHalvingBlockFinishEval_encode
(h Q E ell : ℕ)
(state : NearHalvingBlockRunState)
:
nearHalvingBlockFinishEval (Complexity.pair (encodeNearHalvingBlockRun h Q E state) (List.replicate ell true)) = nearHalvingBlockFinish E ell state
Encoded final extraction agrees with the structured runtime operation.
The total final extraction step is polynomial-time on every encoded input word.
theorem
Algebraic.Cutwidth.Extractor.nearHalvingBlockExtractorBits_length
(N h Q E ell count : ℕ)
(source seeds : List Bool)
:
Every executed level doubles the number of fixed-length leaf outputs.
theorem
Algebraic.Cutwidth.Extractor.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
The complete extractor program composes bounded recursion with shared leaf extraction.