Output capacity and source linearity of the amplified sampler

Logarithmic depth already gives at least the requested output width at every positive scale. Source XOR is preserved even when a total prefix uses false completion.

theorem Algebraic.Cutwidth.Extractor.Internal.amplifiedMatchedSampler_output_capacity (L d : ℕ) (positive : 0 < L) : d ≤ matchedBlockOutputBits (growingMatchedBlockDepth d) L

theorem Algebraic.Cutwidth.Extractor.Internal.amplifiedMatchedSampler_eq_prefix (n L d : ℕ) (positive : 0 < L) (x : Fin n → Bool) (outer : Fin (8 * matchedBlockSeedBits L) → Bool) (candidate : Fin (gammaBlockSeedBudget (matchedBlockSeedBits L)) → Bool) : amplifiedMatchedSampler n L d x outer candidate = fun (j : Fin d) => matchedBlockExtractor n (growingMatchedBlockDepth d) L 4 x (gammaBlockPaddedExtractor (matchedBlockSeedBits L) outer candidate) (Fin.castLE ⋯ j)

theorem Algebraic.Cutwidth.Extractor.Internal.amplifiedMatchedSampler_xor (n L d : ℕ) (x x' : Fin n → Bool) (outer : Fin (8 * matchedBlockSeedBits L) → Bool) (candidate : Fin (gammaBlockSeedBudget (matchedBlockSeedBits L)) → Bool) : amplifiedMatchedSampler n L d (fun (i : Fin n) => x i ^^ x' i) outer candidate = fun (j : Fin d) => amplifiedMatchedSampler n L d x outer candidate j ^^ amplifiedMatchedSampler n L d x' outer candidate j