Polynomial-time generation of the global enumeration bounds

The outer count is exactly a fixed power of 2 ^ clog 2 (n+1), which has a unary polynomial-time certificate. Only the candidate count needs a cap. Its capped power is uniformly computable even before the asymptotic parameter conditions hold.

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionFamilyScale_unary {n : List Bool → ℕ} (hn : Complexity.UnaryFn n) : Complexity.UnaryFn fun (z : List Bool) => sourceReductionFamilyScale (n z)

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionFamilyOuterCount_unary {n : List Bool → ℕ} (hn : Complexity.UnaryFn n) : Complexity.UnaryFn fun (z : List Bool) => sourceReductionOuterCount (matchedBlockSeedBits (sourceReductionFamilyScale (n z)))

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionBoundedCandidates_unary {n : List Bool → ℕ} (hn : Complexity.UnaryFn n) : Complexity.UnaryFn fun (z : List Bool) => sourceReductionBoundedCandidates (n z)