The explicit lower bound with compressed aggregate states

The fixed explicit family keeps coefficient 4.56249… when the logarithmic size of a shared aggregate register is sublinear. This charges the final-state guess and the accumulator, with no restriction on the number of special gates.

theorem Algebraic.Cutwidth.Aggregate.Compressed.sourceReductionHardFamily_eventually_lt_size_of_orderingBound {J : Type} {State : J → Type} [(j : J) → CommMonoid (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, ∀ (M : Type) [inst : CommMonoid M] [inst_1 : Fintype M] (c : Circuit (Aggregate.signature State) n 1) (a : Aggregate.Compressed.Factorization c.program M), (c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => Extractor.sourceReductionHardFamily n x) → Aggregate.Compressed.budget M ≤ 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 for jointly compressed aggregate states.

theorem Algebraic.Cutwidth.Aggregate.Compressed.sourceReductionHardFamily_eventually_lt_size_gaussian {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] (D : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (M : Type) [inst : CommMonoid M] [inst_1 : Fintype M] (c : Circuit (Aggregate.signature State) n 1) (a : Aggregate.Compressed.Factorization c.program M), (c.Computes Aggregate.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => Extractor.sourceReductionHardFamily n x) → Aggregate.Compressed.budget M ≤ 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 joint-state budget is o(n), without a gate-count restriction.