Arithmetic lower bounds with free constants

Addition and multiplication are polynomial operations. More strongly, every arithmetic circuit whose outputs are nonconstant can absorb all its constant gates into polynomial coefficients, emitting exactly one gate per original addition or multiplication. The Gaussian lower bound therefore applies to Arithmetic.gateCost, where arbitrary constant gates are free.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.isPolynomial_arithmetic {F : Type u_1} {K : Type u_2} [CommSemiring F] (constant : K → F) : IsPolynomial (Arithmetic.interpretation constant)

Addition, multiplication, and any family of constants are polynomial operations.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.exists_polynomial_circuit_of_nonconstant {F : Type u_1} {K : Type u_2} [CommSemiring F] {n m : ℕ} (hn : 0 < n) (constant : K → F) (c : Circuit (Arithmetic.signature K) n m) (nonconstant : ∀ (j : Fin m), ∃ (x : Fin n → F) (y : Fin n → F), c.eval (Arithmetic.interpretation constant) x j ≠ c.eval (Arithmetic.interpretation constant) y j) : ∃ (d : Circuit (signature F) n m), d.size = c.cost Arithmetic.gateCost ∧ d.FanInAtMost 2 ∧ ∀ (x : Fin n → F), d.eval (interpretation F) x = c.eval (Arithmetic.interpretation constant) x

Constant elimination preserves all outputs and exactly the number of arithmetic operations.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.eventually_lt_arithmeticCost_of_totallyRegular {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] (M : Matrix (Fin N) (Fin N) F), TotallyRegular M → ∀ (K : Type v) (constant : K → F) (c : Circuit (Arithmetic.signature K) N N), (c.Computes (Arithmetic.interpretation constant) fun (x : Fin N → F) => M.mulVec x) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑N < ↑(c.cost Arithmetic.gateCost)

Totally regular maps need the Gaussian coefficient in additions and multiplications, with arbitrary constants free, over any field.

theorem Algebraic.Cutwidth.MultiOutput.Polynomial.eventually_lt_arithmeticCost_cauchyCharZero {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [CharZero F] (K : Type v) (constant : K → F) (c : Circuit (Arithmetic.signature K) N N), (c.Computes (Arithmetic.interpretation constant) fun (x : Fin N → F) => (cauchyCharZero F N).mulVec x) → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑N < ↑(c.cost Arithmetic.gateCost)

The explicit rational Cauchy family has the same lower bound with free arithmetic constants.