Whole-basis lower bounds from aggregate capacity

The same fixed polynomial-time family requires almost n bits of exact aggregate capacity, with no bound on the number of special gates. Binary gates cost one bit; special gates cost log₂ |M|, without rounding or guessed-output bits. If every special register has at most r ≥ 2 states, the gate coefficient is 1 / log₂ r. In particular two-state aggregate gates preserve a coefficient of one at arbitrary depth and fan-in, with repeated slots and arbitrary special-to-special connections.

The circuit-to-summary argument belongs to the classical communication-complexity approach of Roychowdhury--Orlitsky--Siu (1994). The explicit family is the existing Chattopadhyay--Liao construction, with its full input length and balanced padding.

theorem Algebraic.Cutwidth.Aggregate.sourceReductionHardFamily_eventually_lt_realCapacity {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] {ε : ℝ} (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) → (1 - ε) * ↑n < Aggregate.Capacity.realCapacity c.program

The fixed explicit family requires nearly one bit of exact aggregate capacity per input, with no sparsity condition on the special gates.

theorem Algebraic.Cutwidth.Aggregate.sourceReductionHardFamily_eventually_lt_capacity {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] {ε : ℝ} (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) → (1 - ε) * ↑n < ↑(Aggregate.Capacity.capacity c.program)

The rounded per-register capacity also has leading coefficient one.

theorem Algebraic.Cutwidth.Aggregate.sourceReductionHardFamily_eventually_lt_size_of_register_card {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] (states : ℕ) (hs : 2 ≤ states) {ε : ℝ} (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) → (∀ (gate : Aggregate.SpecialGate c.program), Fintype.card (Aggregate.Register c.program gate) ≤ states) → (1 / Real.logb 2 ↑states - ε) * ↑n < ↑c.size

A uniform bound on state cardinalities gives a whole-basis gate lower bound, with the unrounded coefficient 1 / log₂ states.

theorem Algebraic.Cutwidth.Aggregate.sourceReductionHardFamily_eventually_lt_size_two_state {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] {ε : ℝ} (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) → (∀ (gate : Aggregate.SpecialGate c.program), Fintype.card (Aggregate.Register c.program gate) ≤ 2) → (1 - ε) * ↑n < ↑c.size

Arbitrarily many two-state aggregate gates, together with all binary Boolean gates, still require more than (1 - ε)n gates.