Lower bounds from sublinear joint aggregate state

The graph-ordering coefficient transfers using only the cardinality of a joint factorization. The number of special gates is unrestricted and all gates are counted.

theorem Algebraic.Cutwidth.Aggregate.Compressed.sliceBound_of_circuit {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] {M : Type} [CommMonoid M] [Fintype M] {n g D K : ℕ} (p : Program (Aggregate.signature State) n g) (compression : Aggregate.Compressed.Factorization p M) (out : Wire n g) (budget : Aggregate.Compressed.budget M ≤ D) (free : RectangleFree (fun (x : Cslib.BitString n) => p.trace Aggregate.interpretation x out) K) (dense : 2 ^ (n - 2) ≤ (accepting fun (x : Cslib.BitString n) => p.trace Aggregate.interpretation x out).card) (hK : 1 < K) (big : 3 * (D + Nat.clog 2 K + 3) ≤ n) {A η C : ℝ} (hAη : 0 ≤ A + η) (hC : 0 ≤ C) (order : Multigraph.OrderingBound A η C) : SliceBound A η C n g D K

Every dense rectangle-free mixed circuit admits the finite slice estimate. The budget counts the joint final-state guess and its independent accumulator.

theorem Algebraic.Cutwidth.Aggregate.Compressed.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) (f : (n : ℕ) → Cslib.BooleanFunction n) (D K : ℕ → ℕ) (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hard : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (f n) (K n) ∧ 2 ^ (n - 2) ≤ (accepting (f n)).card) {ε : ℝ} (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) => f n x) → Aggregate.Compressed.budget M ≤ D n → (1 + 1 / A - ε) * ↑n < ↑c.size

The general-coefficient lower bound for binary gates augmented by arbitrary finite commutative-monoid gates with a sublinear joint-state budget.