An actual source-linear somewhere sampler

The actual growing-depth matched extractor, at constant error one sixteenth, is amplified by the actual padded Gamma extractor. At the explicit finite guards, the resulting sampler has failure probability one half and target test density 2^(-5*b), where b = 2^24 * L is the base seed width. Its source threshold is the growing extractor's threshold times two.

No extractor or coverage hypothesis is supplied by the caller. The only guards concern the concrete numerical parameters. XOR-linearity holds at every size, independently of those statistical guards. The construction implements the amplification used in Chattopadhyay--Liao, Extractors for Sum of Two Sources, Lemma 5.4 and Appendix A, proof of Lemma 3.17: https://arxiv.org/abs/2110.12652. Construction.Asymptotics and Construction.Uniform select the eventual parameter family and enumerate its outer coordinates.

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

The selected logarithmic depth supplies every requested output bit at positive scale.

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

At positive scale, false completion is inactive in the requested prefix.

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

Each fixed outer word and candidate gives an XOR-linear map of the original source.

theorem Algebraic.Cutwidth.Extractor.amplifiedMatchedSampler_somewhereSampler (n L d : ℕ) (positive : 0 < L) (base : GrowingMatchedBlockRuntimeValid n d L 4) (gamma : GammaBlockSizeGuard (matchedBlockSeedBits L)) : SomewhereSampler (amplifiedMatchedSampler n L d) (2 ^ amplifiedMatchedSamplerEntropy L d) (2 ^ (5 * matchedBlockSeedBits L))⁻¹ (1 / 2)

The actual composition samples small tests for every normalized source at the stated cap.