Assembling the actual finite sumset extractor #
One source reserve supplies both the actual affine test theorem and the actual amplified sampler. Exact parameter budgets allow the selection theorem to retain enough coordinates for the checked majority argument.
theorem
Algebraic.Cutwidth.Extractor.Internal.sourceReductionExtractor_flat
(n L : ℕ)
(positive : 0 < L)
(base : GrowingMatchedBlockRuntimeValid n (sourceReductionSeedBits n L) L 4)
(gamma : GammaBlockSizeGuard (matchedBlockSeedBits L))
:
FlatSumsetExtractor (sourceReductionExtractor n L) (2 ^ sourceReductionEntropy n L) (35 / 72)