Polynomial threshold functions

A real polynomial is evaluated at the signs chi (x i) on the library's usual cube. Its threshold is 1 at nonnegative values and -1 at negative values. In particular, zeros of the polynomial are allowed and have a fixed convention.

These definitions support the Gotsman--Linial bound proved in OpenAI's Average Sensitivity of Polynomial Threshold Functions (25 September 2026). The public degree predicate permits arbitrary polynomials, without requiring that the input polynomial already be in multilinear normal form.

noncomputable def Complexity.BooleanAnalysis.signMultilinearize {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : MvPolynomial (Fin n) ℝ

Reduce every exponent modulo two, using the sign-cube relation xᵢ² = 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.BooleanAnalysis.polynomialThreshold {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : BooleanFunction n

A polynomial threshold function on the sign cube, with sign(0) = 1.

Equations

• Complexity.BooleanAnalysis.polynomialThreshold p x = if 0 ≤ (MvPolynomial.eval fun (i : Fin n) => Complexity.BooleanAnalysis.chi (x i)) p then 1 else -1

def Complexity.BooleanAnalysis.IsPolynomialThreshold {n : ℕ} (f : BooleanFunction n) (d : ℕ) : Prop

A Boolean function represented by a real polynomial threshold of degree at most d.

Equations

• Complexity.BooleanAnalysis.IsPolynomialThreshold f d = ∃ (p : MvPolynomial (Fin n) ℝ), p.totalDegree ≤ d ∧ f = Complexity.BooleanAnalysis.polynomialThreshold p