Quartic-over-logarithmic lower bound for rational permanent formulas

Source: url:https://github.com/openai/ten-proofs Authors: OpenAI, Dean Cureton Status: verified Main declarations: PermanentFormulaLowerBound.permanent_rational_formula_logarithmic_lower_bound Tags: algebraic-complexity, arithmetic-formulas, permanent, lower-bounds, transcendence-degree MSC: 68Q17, 68Q25, 15A15

inductive PermanentFormulaLowerBound.RationalFormula (ι : Type u) (R : Type v) : Type (max u v)

A rational arithmetic formula with variables indexed by ι and constants in R.

• var {ι : Type u} {R : Type v} : ι → RationalFormula ι R
• const {ι : Type u} {R : Type v} : R → RationalFormula ι R
• add {ι : Type u} {R : Type v} : RationalFormula ι R → RationalFormula ι R → RationalFormula ι R
• sub {ι : Type u} {R : Type v} : RationalFormula ι R → RationalFormula ι R → RationalFormula ι R
• mul {ι : Type u} {R : Type v} : RationalFormula ι R → RationalFormula ι R → RationalFormula ι R
• div {ι : Type u} {R : Type v} : RationalFormula ι R → RationalFormula ι R → RationalFormula ι R

noncomputable def PermanentFormulaLowerBound.RationalFormula.eval {ι : Type u} {R : Type v} [Field R] : RationalFormula ι R → FractionRing (MvPolynomial ι R)

Evaluates a rational formula in the fraction field of multivariate polynomials.

Equations

• (PermanentFormulaLowerBound.RationalFormula.var i).eval = (algebraMap (MvPolynomial ι R) (FractionRing (MvPolynomial ι R))) (MvPolynomial.X i)
• (PermanentFormulaLowerBound.RationalFormula.const c).eval = (algebraMap (MvPolynomial ι R) (FractionRing (MvPolynomial ι R))) (MvPolynomial.C c)
• (f.add g).eval = f.eval + g.eval
• (f.sub g).eval = f.eval - g.eval
• (f.mul g).eval = f.eval * g.eval
• (f.div g).eval = f.eval / g.eval

inductive PermanentFormulaLowerBound.RationalFormula.Valid {ι : Type u} {R : Type v} [Field R] : RationalFormula ι R → Prop

A rational formula is valid when every divisor occurring in it evaluates to a nonzero value.

• var {ι : Type u} {R : Type v} [Field R] (i : ι) : (RationalFormula.var i).Valid
• const {ι : Type u} {R : Type v} [Field R] (c : R) : (RationalFormula.const c).Valid
• add {ι : Type u} {R : Type v} [Field R] {f g : RationalFormula ι R} : f.Valid → g.Valid → (f.add g).Valid
• sub {ι : Type u} {R : Type v} [Field R] {f g : RationalFormula ι R} : f.Valid → g.Valid → (f.sub g).Valid
• mul {ι : Type u} {R : Type v} [Field R] {f g : RationalFormula ι R} : f.Valid → g.Valid → (f.mul g).Valid
• div {ι : Type u} {R : Type v} [Field R] {f g : RationalFormula ι R} : f.Valid → g.Valid → g.eval ≠ 0 → (f.div g).Valid

def PermanentFormulaLowerBound.RationalFormula.leafCount {ι : Type u} {R : Type v} : RationalFormula ι R → ℕ

The total number of variable and constant leaves in a rational formula.

Equations

• (PermanentFormulaLowerBound.RationalFormula.var i).leafCount = 1
• (PermanentFormulaLowerBound.RationalFormula.const c).leafCount = 1
• (f.add g).leafCount = f.leafCount + g.leafCount
• (f.sub g).leafCount = f.leafCount + g.leafCount
• (f.mul g).leafCount = f.leafCount + g.leafCount
• (f.div g).leafCount = f.leafCount + g.leafCount

def PermanentFormulaLowerBound.RationalFormula.variableLeaves {ι : Type u} {R : Type v} : RationalFormula ι R → ℕ

The number of variable leaves in a rational formula.

Equations

• (PermanentFormulaLowerBound.RationalFormula.var i).variableLeaves = 1
• (PermanentFormulaLowerBound.RationalFormula.const c).variableLeaves = 0
• (f.add g).variableLeaves = f.variableLeaves + g.variableLeaves
• (f.sub g).variableLeaves = f.variableLeaves + g.variableLeaves
• (f.mul g).variableLeaves = f.variableLeaves + g.variableLeaves
• (f.div g).variableLeaves = f.variableLeaves + g.variableLeaves

def PermanentFormulaLowerBound.RationalFormula.internalGateCount {ι : Type u} {R : Type v} : RationalFormula ι R → ℕ

The number of arithmetic-operation gates in a rational formula.

Equations

• (PermanentFormulaLowerBound.RationalFormula.var i).internalGateCount = 0
• (PermanentFormulaLowerBound.RationalFormula.const c).internalGateCount = 0
• (f.add g).internalGateCount = f.internalGateCount + g.internalGateCount + 1
• (f.sub g).internalGateCount = f.internalGateCount + g.internalGateCount + 1
• (f.mul g).internalGateCount = f.internalGateCount + g.internalGateCount + 1
• (f.div g).internalGateCount = f.internalGateCount + g.internalGateCount + 1

def PermanentFormulaLowerBound.RationalFormula.vertexCount {ι : Type u} {R : Type v} : RationalFormula ι R → ℕ

The total number of vertices in the syntax tree of a rational formula.

Equations

• (PermanentFormulaLowerBound.RationalFormula.var i).vertexCount = 1
• (PermanentFormulaLowerBound.RationalFormula.const c).vertexCount = 1
• (f.add g).vertexCount = f.vertexCount + g.vertexCount + 1
• (f.sub g).vertexCount = f.vertexCount + g.vertexCount + 1
• (f.mul g).vertexCount = f.vertexCount + g.vertexCount + 1
• (f.div g).vertexCount = f.vertexCount + g.vertexCount + 1

noncomputable def PermanentFormulaLowerBound.permanentPolynomial (n : ℕ) : MvPolynomial (Fin n × Fin n) ℂ

The generic n-by-n permanent polynomial over the complex numbers.

Equations

• PermanentFormulaLowerBound.permanentPolynomial n = (Matrix.mvPolynomialX (Fin n) (Fin n) ℂ).permanent

theorem PermanentFormulaLowerBound.permanent_rational_formula_lower_bound {n : ℕ} (hn : 32 ≤ n) (f : RationalFormula (Fin n × Fin n) ℂ) (hvalid : f.Valid) (hf : f.eval = (algebraMap (MvPolynomial (Fin n × Fin n) ℂ) (FractionRing (MvPolynomial (Fin n × Fin n) ℂ))) (permanentPolynomial n)) : ↑n ^ 4 / (192 * Real.logb 2 ↑n) ≤ ↑f.variableLeaves ∧ ↑n ^ 4 / (192 * Real.logb 2 ↑n) ≤ ↑f.leafCount ∧ ↑n ^ 4 / (192 * Real.logb 2 ↑n) ≤ ↑f.vertexCount ∧ ↑n ^ 4 / (384 * Real.logb 2 ↑n) ≤ ↑f.internalGateCount

Simultaneous size lower bounds for rational formulas computing the permanent.

theorem PermanentFormulaLowerBound.permanent_rational_formula_logarithmic_lower_bound {n : ℕ} (hn : 32 ≤ n) (f : RationalFormula (Fin n × Fin n) ℂ) (hvalid : f.Valid) (hf : f.eval = (algebraMap (MvPolynomial (Fin n × Fin n) ℂ) (FractionRing (MvPolynomial (Fin n × Fin n) ℂ))) (permanentPolynomial n)) : ↑n ^ 4 / (192 * Real.logb 2 ↑n) ≤ ↑f.variableLeaves

Any valid rational formula computing the n-by-n permanent has at least n ^ 4 / (192 * logb 2 n) variable leaves when 32 ≤ n.