Uniform computation and eventual extraction of the same fixed family

The candidate cap makes enumeration polynomial-time at every length. Its eventual inactivity identifies the computed family with the actual finite extractor. Thus the statistical and computational theorems concern one fixed family, with no supplied algorithm or asymptotic hypothesis.

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

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

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

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

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

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