One uniform evaluator for growing-depth matched extraction

The unary input t selects depth clog 2 (t+1) + 64. Its leaf count is at most 2^65 * (t+1), allowing polynomial-time parameter generation and bounded numerical and payload iteration. This certificate concerns that logarithmic depth selection; it does not permit an arbitrary unary depth with exponentially many output blocks.

The actual paired string evaluator is total on every input. Under the explicit growing-depth guard it equals the existing matched Boolean extractor, with the complete padded seed accepted and any extra suffix ignored. Invalid parameters return an empty word. The statistical guarantee is supplied by Scheduled.Matched.Growing; this layer supplies its uniform runtime without changing the earlier fixed-depth evaluator.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockDepth_pow_le (t : ℕ) : 2 ^ growingMatchedBlockDepth t ≤ 2 ^ 65 * (t + 1)

The number of leaves is linear in the unary depth-selection parameter.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockDepth_pow_four_le (t : ℕ) : 4 ^ growingMatchedBlockDepth t ≤ (2 ^ 65 * (t + 1)) ^ 2

The initial entropy's depth factor is quadratic in the unary parameter.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockDepth_unaryFn {t : List Bool → ℕ} (ht : Complexity.UnaryFn t) : Complexity.UnaryFn fun (z : List Bool) => growingMatchedBlockDepth (t z)

The logarithmic recursion depth is uniformly computable in unary.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockDepth_pow_unaryFn {t : List Bool → ℕ} (ht : Complexity.UnaryFn t) : Complexity.UnaryFn fun (z : List Bool) => 2 ^ growingMatchedBlockDepth (t z)

Generating the leaf count is polynomial-time on all inputs, including t = 0.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockExtractorRuntime_of_valid (t L e : ℕ) (source seeds : List Bool) (valid : GrowingMatchedBlockRuntimeValid source.length t L e) : growingMatchedBlockExtractorRuntime t L e source seeds = have h := growingMatchedBlockDepth t; 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 parameters run the scheduled bit program after taking its exact seed prefix.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockExtractorRuntime_of_not_valid (t L e : ℕ) (source seeds : List Bool) (invalid : ¬GrowingMatchedBlockRuntimeValid source.length t L e) : growingMatchedBlockExtractorRuntime t L e source seeds = []

Invalid parameters return the empty word.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockExtractorRuntime_length (t L e : ℕ) (source seeds : List Bool) : (growingMatchedBlockExtractorRuntime t L e source seeds).length = if GrowingMatchedBlockRuntimeValid source.length t L e then 2 ^ growingMatchedBlockDepth t * L else 0

The exact output width is one scale-sized word per leaf whenever the guard holds.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockExtractorRuntime_length_le (t L e : ℕ) (source seeds : List Bool) : (growingMatchedBlockExtractorRuntime t L e source seeds).length ≤ 2 ^ 65 * (t + 1) * L

Every runtime output has polynomially bounded length, including malformed inputs.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockRuntimeValid_fpPred {n t L e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (ht : Complexity.UnaryFn t) (hL : Complexity.UnaryFn L) (he : Complexity.UnaryFn e) : Complexity.FPPred fun (z : List Bool) => GrowingMatchedBlockRuntimeValid (n z) (t z) (L z) (e z)

The full finite validity condition is polynomial-time on unary numerical inputs.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockExtractorRuntime_mem_FP {t L e : List Bool → ℕ} {source seeds : List Bool → List Bool} (ht : Complexity.UnaryFn t) (hL : Complexity.UnaryFn L) (he : Complexity.UnaryFn e) (hsource : source ∈ Complexity.FP) (hseeds : seeds ∈ Complexity.FP) : (fun (z : List Bool) => growingMatchedBlockExtractorRuntime (t z) (L z) (e z) (source z) (seeds z)) ∈ Complexity.FP

The total runtime includes all parameter, exact seed-width, and payload computations.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockExtractorEval_pair (source seeds parameter scale error : List Bool) : growingMatchedBlockExtractorEval (Complexity.pair (Complexity.pair source seeds) (Complexity.pair parameter (Complexity.pair scale error))) = growingMatchedBlockExtractorRuntime parameter.length scale.length error.length source seeds

The paired interface reads two words and three unary numbers.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockExtractorEval_mem_FP : growingMatchedBlockExtractorEval ∈ Complexity.FP

One paired evaluator is polynomial-time on every string.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockExtractorEval_length_le (z : List Bool) : (growingMatchedBlockExtractorEval z).length ≤ 2 ^ 65 * (z.length + 1) ^ 2

The complete encoded evaluator's output length is quadratic in its encoded input length.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockExtractorRuntime_eq_matchedBlockExtractor (n t L e : ℕ) (valid : GrowingMatchedBlockRuntimeValid n t L e) (x : Fin n → Bool) (seed : Fin (matchedBlockSeedBits L) → Bool) : growingMatchedBlockExtractorRuntime t L e (List.ofFn x) (List.ofFn seed) = List.ofFn (matchedBlockExtractor n (growingMatchedBlockDepth t) L e x seed)

Canonical Boolean inputs evaluate to exactly the actual growing-depth matched map.

theorem Algebraic.Cutwidth.Extractor.growingMatchedBlockExtractorRuntime_append_eq_matchedBlockExtractor (n t L e : ℕ) (valid : GrowingMatchedBlockRuntimeValid n t L e) (x : Fin n → Bool) (seed : Fin (matchedBlockSeedBits L) → Bool) (tail : List Bool) : growingMatchedBlockExtractorRuntime t L e (List.ofFn x) (List.ofFn seed ++ tail) = List.ofFn (matchedBlockExtractor n (growingMatchedBlockDepth t) L e x seed)

The full padded seed has the same meaning even when an arbitrary suffix is appended.