The explicit lower bound with finite commutative aggregate gates

The fixed polynomial-time sourceReductionHardFamily keeps the unconditional coefficient 1 + π/(3 arccos((1 + 2√2)/4)), about 4.5625, when binary circuits are augmented with special gates whose total finite-state budget is sublinear.

Each special gate computes a Boolean predicate of the product of slot-dependent contributions in a finite commutative monoid. Its budget is one guessed output bit plus the ceiling binary logarithm of its number of states. The conclusion counts all gates. Fan-in of special gates, fanout, depth, repeated slots, and special-to-special connections are unrestricted. No extractor, compiler, invertibility, or unproved graph hypothesis remains in the Gaussian theorem.

The existing extractor construction is due to Chattopadhyay--Liao; the cutwidth lower-bound architecture follows Ryan Williams's private working note. This extension replaces invertible accumulators by outgoing-transition counting. See the sources in FourN and Extractor.SourceReduction.Construction.Defs.

theorem Algebraic.Cutwidth.Aggregate.sourceReductionHardFamily_eventually_lt_size_of_orderingBound {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) (D : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (c : Circuit (Aggregate.signature State) n 1), (c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => Extractor.sourceReductionHardFamily n x) → Aggregate.budget c.program ≤ D n → (1 + 1 / A - ε) * ↑n < ↑c.size

Any proved graph-ordering coefficient transfers to the fixed explicit family for mixed circuits with a sublinear budget of special-output guesses and monoid registers.

theorem Algebraic.Cutwidth.Aggregate.sourceReductionHardFamily_eventually_lt_size_gaussian {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] (D : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (c : Circuit (Aggregate.signature State) n 1), (c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => Extractor.sourceReductionHardFamily n x) → Aggregate.budget c.program ≤ D n → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.size

The unconditional aggregate-gate extension. The same fixed family in polynomial time needs more than (4.56249… - ε) n total gates, even with arbitrary finite commutative-monoid aggregate gates whose total output-guess and register budget is o(n).

theorem Algebraic.Cutwidth.Aggregate.sourceReductionHardFamily_eventually_lt_size_fortyOne_div_nine {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] (D : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (c : Circuit (Aggregate.signature State) n 1), (c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => Extractor.sourceReductionHardFamily n x) → Aggregate.budget c.program ≤ D n → (41 / 9 - ε) * ↑n < ↑c.size

A convenient rational weakening of the unconditional aggregate-gate bound.