Correctness and uniform computation of the amplified sampler #
The two component evaluator equalities compose on canonical words. Only the growing matched guard is needed for this identity; Gamma agrees with its own total Boolean map on every size. Prefix completion preserves the exact requested output length even when the component returns no bits.
theorem
Algebraic.Cutwidth.Extractor.Internal.amplifiedMatchedSamplerRuntime_length
(L d : ℕ)
(source outer candidate : List Bool)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.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)
theorem
Algebraic.Cutwidth.Extractor.Internal.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
theorem
Algebraic.Cutwidth.Extractor.Internal.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