A uniform polynomial-time program for the complete recursive extractor

One program generates the actual rounded parameters, runs initial condensation and every internal block level, and extracts all leaves with one final shared seed pair. The requested depth is clipped to the ceiling binary logarithm of the source length, so every input has a valid reserve budget and polynomial bounds on the complete run. A valid requested depth is unchanged by this clipping.

The public evaluator accepts paired source, seed word, unary requested depth, and unary error exponent. Its FP theorem has no numerical validity premise and covers malformed pairing inputs through the total projections. Canonical seed words connect this program to the statistical map in the separate correctness layer.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockExtractorBits_length (n h Q E ell : ℕ) (source seeds : List Bool) : (scheduledBlockExtractorBits n h Q E ell source seeds).length = 2 ^ h * ell

The full bit program emits the requested number of leaf output bits.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockExtractorBits_mem_FP {n h Q E ell : 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) (hell : Complexity.UnaryFn ell) (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) => scheduledBlockExtractorBits (n z) (h z) (Q z) (E z) (ell z) (source z) (seeds z)) ∈ Complexity.FP

The specified bit program is uniform in all unary parameters under the global reserve budget.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockExtractorRuntime_mem_FP {requested e : List Bool → ℕ} {source seeds : List Bool → List Bool} (hrequested : Complexity.UnaryFn requested) (he : Complexity.UnaryFn e) (hsource : source ∈ Complexity.FP) (hseeds : seeds ∈ Complexity.FP) : (fun (z : List Bool) => scheduledBlockExtractorRuntime (requested z) (e z) (source z) (seeds z)) ∈ Complexity.FP

Parameter generation and complete extraction form one uniform polynomial-time map.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockExtractorEval_pair (source seeds requested error : List Bool) : scheduledBlockExtractorEval (Complexity.pair (Complexity.pair source seeds) (Complexity.pair requested error)) = scheduledBlockExtractorRuntime requested.length error.length source seeds

The paired evaluator decodes the source, flat seed word, requested depth, and error.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockExtractorRuntime_of_depth_le (requested e : ℕ) (source seeds : List Bool) (depth : requested ≤ Nat.clog 2 (source.length + 1)) : scheduledBlockExtractorRuntime requested e source seeds = scheduledBlockExtractorBits source.length requested (recursiveBlockReserve (Nat.clog 2 (source.length + 1)) (e + requested + 2)) (e + requested + 2) (Nat.clog 2 (source.length + 1)) source seeds

A requested depth within the logarithmic budget is evaluated without alteration.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockExtractorEval_mem_FP : scheduledBlockExtractorEval ∈ Complexity.FP

The single total paired evaluator is polynomial-time on every input word.