One uniform polynomial-time sumset-extractor family

All parameters are generated from the original input length. The outer count has an unconditional polynomial bound, and a cap makes the candidate count uniformly bounded at every size. The cap is eventually inactive. The computed family therefore has the actual extractor's constant error and sublinear source entropy for all sufficiently large lengths.

Balanced padding gives one fixed, exactly balanced family at every positive length and preserves its total polynomial-time evaluator. The subsequent circuit lower bound is measured at this full padded input length.

theorem Algebraic.Cutwidth.Extractor.sourceReductionFamilyEval_length (source : List Bool) : (sourceReductionFamilyEval source).length = 1

The total unpadded evaluator returns exactly one bit at every input length.

theorem Algebraic.Cutwidth.Extractor.sourceReductionFamilyEval_ofFn (n : ℕ) (x : Fin n → Bool) : sourceReductionFamilyEval (List.ofFn x) = [sourceReductionFamily n x]

The evaluator computes the same Boolean family at every input length.

theorem Algebraic.Cutwidth.Extractor.sourceReductionFamilyEval_mem_FP : sourceReductionFamilyEval ∈ Complexity.FP

All parameter generation, enumeration, actual calls, XOR, and majority are polynomial-time.

theorem Algebraic.Cutwidth.Extractor.sourceReductionFamily_eventually_eq : ∀ᶠ (n : ℕ) in Filter.atTop, sourceReductionFamily n = sourceReductionExtractor n (sourceReductionFamilyScale n)

Eventually the computed family equals the actual finite sumset construction exactly. The proof needs the candidate cap n + 1 to be inactive, and the cap binds at every positive length with log₂ (n + 1) < 2 ^ 27 * 70 ^ 3 ≈ 4.6 * 10 ^ 13. The threshold here, which every circuit bound for the hard family inherits, therefore exceeds 2 ^ (4.6 * 10 ^ 13).

theorem Algebraic.Cutwidth.Extractor.sourceReductionFamily_eventually_flat : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (sourceReductionFamily n) (2 ^ sourceReductionEntropy n (sourceReductionFamilyScale n)) (35 / 72)

The one computed family eventually extracts with constant error below one half.

theorem Algebraic.Cutwidth.Extractor.sourceReductionFamilyEntropy_isLittleO : (fun (n : ℕ) => ↑(sourceReductionEntropy n (sourceReductionFamilyScale n))) =o[Filter.atTop] fun (n : ℕ) => ↑n

The actual source entropy of the uniformly computed family is sublinear.

theorem Algebraic.Cutwidth.Extractor.sourceReductionHardFamily_succ (n : ℕ) : sourceReductionHardFamily (n + 1) = balancePad (sourceReductionFamily n)

At each positive length, the final family is precisely balanced padding.

theorem Algebraic.Cutwidth.Extractor.sourceReductionHardFamily_card_accepting (n : ℕ) : (accepting (sourceReductionHardFamily (n + 1))).card = 2 ^ n

Exactly half of the full padded input cube is accepted, including while the cap is active.

theorem Algebraic.Cutwidth.Extractor.sourceReductionHardEval_ofFn (n : ℕ) (x : Fin n → Bool) : sourceReductionHardEval (List.ofFn x) = [sourceReductionHardFamily n x]

A single total evaluator computes the hard family at every input length, including zero.

theorem Algebraic.Cutwidth.Extractor.sourceReductionHardEval_mem_FP : sourceReductionHardEval ∈ Complexity.FP

The final balanced family has an unconditional uniform polynomial-time evaluator. The polynomial has enormous degree: on an input of length n + 1 the evaluator enumerates (2 ^ clog₂ (n + 1)) ^ (2 ^ 27) ≥ (n + 1) ^ (2 ^ 27) outer coordinates, so its degree is at least 2 ^ 27 ≈ 1.3 * 10 ^ 8.

theorem Algebraic.Cutwidth.Extractor.mem_sourceReductionHardLanguage_ofFn (n : ℕ) (x : Fin n → Bool) : List.ofFn x ∈ sourceReductionHardLanguage ↔ sourceReductionHardFamily n x = true

Membership in the hard language agrees exactly with every Boolean slice.

theorem Algebraic.Cutwidth.Extractor.sourceReductionHardLanguage_mem_P : sourceReductionHardLanguage ∈ Complexity.P

The concrete hard language has a deterministic polynomial-time decider. The decider runs sourceReductionHardEval, so its polynomial also has degree at least 2 ^ 27.