An actual sumset-extractor family with sublinear source entropy

Choose L = clog 2 (n+1) in the fixed finite source reduction. Both concrete sampler guards eventually hold, and the actual selected entropy exponent is little-o of n. The candidate count remains the full exponential of the cubic Gamma seed budget; it too is sublinear in n, so an eventual linear cap can be used in a separate total evaluator.

These are numerical deductions for the checked Chattopadhyay--Liao Lemma 5.4 construction, https://arxiv.org/abs/2110.12652. Cslib's natural exponential-versus-polynomial theorem supplies the limit comparison. The statistical conclusion concerns the actual fixed map, with error 35/72. This module does not assert polynomial-time evaluation of its full outer and candidate enumeration.

theorem Algebraic.Cutwidth.Extractor.sourceReductionCandidateCount_isLittleO : (fun (n : ℕ) => ↑(sourceReductionCandidateCount (matchedBlockSeedBits (Nat.clog 2 (n + 1))))) =o[Filter.atTop] fun (n : ℕ) => ↑n

The full, unbounded candidate count is sublinear in the original input length.

theorem Algebraic.Cutwidth.Extractor.eventually_sourceReductionCandidateCount_le : ∀ᶠ (n : ℕ) in Filter.atTop, sourceReductionCandidateCount (matchedBlockSeedBits (Nat.clog 2 (n + 1))) ≤ n + 1

Clamping the candidate count at n+1 is eventually inactive.

theorem Algebraic.Cutwidth.Extractor.sourceReductionEntropy_isLittleO : (fun (n : ℕ) => ↑(sourceReductionEntropy n (Nat.clog 2 (n + 1)))) =o[Filter.atTop] fun (n : ℕ) => ↑n

The complete source reserve, including every leakage word and the sampler, is sublinear.

theorem Algebraic.Cutwidth.Extractor.eventually_sourceReductionEntropy_le : ∀ᶠ (n : ℕ) in Filter.atTop, sourceReductionEntropy n (Nat.clog 2 (n + 1)) ≤ n

The selected source support threshold is eventually feasible within n bits.

theorem Algebraic.Cutwidth.Extractor.eventually_sourceReduction_guards : ∀ᶠ (n : ℕ) in Filter.atTop, have L := Nat.clog 2 (n + 1); 0 < L ∧ GrowingMatchedBlockRuntimeValid n (sourceReductionSeedBits n L) L 4 ∧ GammaBlockSizeGuard (matchedBlockSeedBits L)

The actual growing matched and Gamma samplers meet all their finite numerical guards.

theorem Algebraic.Cutwidth.Extractor.eventually_sourceReductionExtractor_flat : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (sourceReductionExtractor n (Nat.clog 2 (n + 1))) (2 ^ sourceReductionEntropy n (Nat.clog 2 (n + 1))) (35 / 72)

One fixed actual Boolean family eventually extracts from both flat sources.