Uniform computation of the shared-scale matched extractor

Bounded numerical-state iteration computes every actual width and its seed cost. A finite sum gives the exact total seed prefix before the unchanged payload program runs. Safe parameters certify this complete computation on all inputs; on the valid branch they equal the supplied parameters. Depth is bounded by 64 when generating powers, and every intermediate numerical and payload state uses the existing global reserve bound.

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledSeedBits_unaryFn {n h Q E ell : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hh : Complexity.UnaryFn h) (hentropy : Complexity.UnaryFn fun (z : List Bool) => recursiveBlockEntropy (h z) (Q z) 0) (hE : Complexity.UnaryFn E) (hell : Complexity.UnaryFn ell) (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) : Complexity.UnaryFn fun (z : List Bool) => scheduledBlockSeedBits (n z) (h z) (Q z) (E z) (ell z)

Bounded schedule iteration computes the exact seed width at any certified depth.

theorem Algebraic.Cutwidth.Extractor.Internal.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)

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

theorem Algebraic.Cutwidth.Extractor.Internal.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

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

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

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

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)