Uniform runtime for the matched-width scheduled extractor

The protocol's supplied scale determines both leaf output width and reserve. The checked guard bounds the depth before any variable power is generated; the complete numerical, seed-width, and payload computations have one uniform FP certificate. Invalid parameters give an empty output. Valid parameters run the existing scheduled bit program with exactly its required seed prefix. At canonical Boolean words the runtime equals matchedBlockExtractor, including when an arbitrary extra seed suffix is supplied.

This is an evaluator for the actual construction. Its statistical guarantee and seed budget are supplied by Scheduled.Matched; no semantic field enumeration or caller-supplied numerical resource premise occurs here.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractorRuntime_of_valid (h L e : ℕ) (source seeds : List Bool) (valid : MatchedBlockRuntimeValid source.length h L e) : matchedBlockExtractorRuntime h L e source seeds = scheduledBlockExtractorBits source.length h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L source (List.take (scheduledBlockSeedBits source.length h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L) seeds)

Valid inputs run the prescribed schedule after discarding unused seed padding.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractorRuntime_of_not_valid (h L e : ℕ) (source seeds : List Bool) (invalid : ¬MatchedBlockRuntimeValid source.length h L e) : matchedBlockExtractorRuntime h L e source seeds = []

Invalid parameters return the empty word.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractorRuntime_length (h L e : ℕ) (source seeds : List Bool) : (matchedBlockExtractorRuntime h L e source seeds).length = if MatchedBlockRuntimeValid source.length h L e then 2 ^ h * L else 0

The accepted schedule outputs one L-bit word per leaf.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractorRuntime_length_le (h L e : ℕ) (source seeds : List Bool) : (matchedBlockExtractorRuntime h L e source seeds).length ≤ 2 ^ 64 * L

The output width is bounded for every supplied depth, including invalid inputs.

theorem Algebraic.Cutwidth.Extractor.matchedBlockRuntimeValid_fpPred {n h L e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hh : Complexity.UnaryFn h) (hL : Complexity.UnaryFn L) (he : Complexity.UnaryFn e) : Complexity.FPPred fun (z : List Bool) => MatchedBlockRuntimeValid (n z) (h z) (L z) (e z)

The validity guard is uniformly polynomial-time in its unary parameters.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractorRuntime_mem_FP {h L e : List Bool → ℕ} {source seeds : List Bool → List Bool} (hh : Complexity.UnaryFn h) (hL : Complexity.UnaryFn L) (he : Complexity.UnaryFn e) (hsource : source ∈ Complexity.FP) (hseeds : seeds ∈ Complexity.FP) : (fun (z : List Bool) => matchedBlockExtractorRuntime (h z) (L z) (e z) (source z) (seeds z)) ∈ Complexity.FP

Complete shared-scale extraction is uniformly polynomial-time on arbitrary runtime inputs.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractorEval_pair (source seeds depth scale error : List Bool) : matchedBlockExtractorEval (Complexity.pair (Complexity.pair source seeds) (Complexity.pair depth (Complexity.pair scale error))) = matchedBlockExtractorRuntime depth.length scale.length error.length source seeds

The paired interface reads source and seed words and three unary numerical parameters.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractorEval_mem_FP : matchedBlockExtractorEval ∈ Complexity.FP

One total paired string evaluator includes all parameter and payload computations.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractorRuntime_eq_matchedBlockExtractor (n h L e : ℕ) (valid : MatchedBlockRuntimeValid n h L e) (x : Fin n → Bool) (seed : Fin (matchedBlockSeedBits L) → Bool) : matchedBlockExtractorRuntime h L e (List.ofFn x) (List.ofFn seed) = List.ofFn (matchedBlockExtractor n h L e x seed)

On canonical words, the runtime computes exactly the actual matched Boolean extractor.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractorRuntime_append_eq_matchedBlockExtractor (n h L e : ℕ) (valid : MatchedBlockRuntimeValid n h L e) (x : Fin n → Bool) (seed : Fin (matchedBlockSeedBits L) → Bool) (tail : List Bool) : matchedBlockExtractorRuntime h L e (List.ofFn x) (List.ofFn seed ++ tail) = List.ofFn (matchedBlockExtractor n h L e x seed)

Extra seed padding is ignored, preserving exact agreement with the Boolean extractor.