A uniform total evaluator for the amplified sampler

Both component algorithms run on actual input words. The evaluator returns exactly the requested output width on every input, with false completion when necessary. Canonical inputs agree with the Boolean sampler under the growing-extractor guard; no Gamma size guard is needed for that identity. The FP certificates are unconditional and accept computed unary widths. They concern one sampled position, not enumeration of an entire parameter family's outer words and candidates.

theorem Algebraic.Cutwidth.Extractor.amplifiedMatchedSamplerRuntime_length (L d : ℕ) (source outer candidate : List Bool) : (amplifiedMatchedSamplerRuntime L d source outer candidate).length = d

Every input, including invalid component parameters, produces exactly d bits.

theorem Algebraic.Cutwidth.Extractor.amplifiedMatchedSamplerRuntime_eq_amplifiedMatchedSampler (n L d : ℕ) (base : GrowingMatchedBlockRuntimeValid n d L 4) (x : Fin n → Bool) (outer : Fin (8 * matchedBlockSeedBits L) → Bool) (candidate : Fin (gammaBlockSeedBudget (matchedBlockSeedBits L)) → Bool) : amplifiedMatchedSamplerRuntime L d (List.ofFn x) (List.ofFn outer) (List.ofFn candidate) = List.ofFn (amplifiedMatchedSampler n L d x outer candidate)

The actual word program computes the canonical Boolean sampler under its growing guard.

theorem Algebraic.Cutwidth.Extractor.amplifiedMatchedSamplerRuntime_mem_FP {L d : List Bool → ℕ} {source outer candidate : List Bool → List Bool} (hL : Complexity.UnaryFn L) (hd : Complexity.UnaryFn d) (hsource : source ∈ Complexity.FP) (houter : outer ∈ Complexity.FP) (hcandidate : candidate ∈ Complexity.FP) : (fun (z : List Bool) => amplifiedMatchedSamplerRuntime (L z) (d z) (source z) (outer z) (candidate z)) ∈ Complexity.FP

Computed unary widths and three runtime words give one polynomial-time composition.

theorem Algebraic.Cutwidth.Extractor.amplifiedMatchedSamplerEval_pair (source outer candidate scale outputWidth : List Bool) : amplifiedMatchedSamplerEval (Complexity.pair (Complexity.pair source (Complexity.pair outer candidate)) (Complexity.pair scale outputWidth)) = amplifiedMatchedSamplerRuntime scale.length outputWidth.length source outer candidate

Decoding the paired input passes all words and unary lengths to the actual runtime.

theorem Algebraic.Cutwidth.Extractor.amplifiedMatchedSamplerEval_length (z : List Bool) : (amplifiedMatchedSamplerEval z).length = (Complexity.pairSnd (Complexity.pairSnd z)).length

The decoded output-width word determines the output length on every encoded input.

theorem Algebraic.Cutwidth.Extractor.amplifiedMatchedSamplerEval_length_le (z : List Bool) : (amplifiedMatchedSamplerEval z).length ≤ z.length

The paired evaluator's output never exceeds its encoded input length.

theorem Algebraic.Cutwidth.Extractor.amplifiedMatchedSamplerEval_mem_FP : amplifiedMatchedSamplerEval ∈ Complexity.FP

A single total polynomial-time evaluator computes the sampler on every paired word.