The enumerated sampler used by the actual reduction

The concrete binary encodings transport the sampling theorem to the exact finite ranges traversed by the reduction. The same index maps preserve unconditional source XOR-linearity.

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionSampler_xor (n L : ℕ) (x y : Fin n → Bool) (i : Fin (sourceReductionOuterCount (matchedBlockSeedBits L))) (z : Fin (sourceReductionCandidateCount (matchedBlockSeedBits L))) : sourceReductionSampler n L (fun (j : Fin n) => x j ^^ y j) i z = fun (j : Fin (sourceReductionSeedBits n L)) => sourceReductionSampler n L x i z j ^^ sourceReductionSampler n L y i z j

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionSampler_somewhereSampler (n L : ℕ) (positive : 0 < L) (base : GrowingMatchedBlockRuntimeValid n (sourceReductionSeedBits n L) L 4) (gamma : GammaBlockSizeGuard (matchedBlockSeedBits L)) : SomewhereSampler (sourceReductionSampler n L) (2 ^ amplifiedMatchedSamplerEntropy L (sourceReductionSeedBits n L)) (sourceReductionSamplerError (matchedBlockSeedBits L)) (1 / 2)