Polynomial-time computation of the complete scheduled extractor #
The final shared extraction stage composes with the certified complete block loop. The total parameter generator supplies every capacity, reserve, and bounded-power obligation for arbitrary runtime inputs. The result is one uniform polynomial-time program, including parameter generation and all internal levels, without a caller-supplied validity premise.
theorem
Algebraic.Cutwidth.Extractor.Internal.scheduledBlockFinishEval_encode
(E ell : ℕ)
(state : ScheduledBlockRunState)
:
scheduledBlockFinishEval (Complexity.pair (encodeScheduledBlockRun E state) (List.replicate ell true)) = scheduledBlockFinish E ell state
theorem
Algebraic.Cutwidth.Extractor.Internal.scheduledBlockExtractorBits_length
(n h Q E ell : ℕ)
(source seeds : List Bool)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.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
theorem
Algebraic.Cutwidth.Extractor.Internal.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
theorem
Algebraic.Cutwidth.Extractor.Internal.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
theorem
Algebraic.Cutwidth.Extractor.Internal.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