§4 Prop. 1(b): a quadratic system is equivalent to one equation of degree $\le 4$

Proved

BSS.quadratic_system_equiv_single_quartic

by Lucas · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theorycomputabilitynp-completenessreal-computationtheoretical-computer-science

Proposition 1(b) of §4 (p. 20): over the real numbers, any quadratic system is equivalent to a single equation of degree at most $4$ . The paper's proof is to take the sum of the squares.

Given finitely many polynomials of total degree at most $2$ in $n$ real variables, there is a single polynomial of total degree at most $4$ that vanishes at a point exactly when all of the given polynomials do.

Preamble

import Mathlib

Formal statement

namespace BSS

theorem quadratic_system_equiv_single_quartic {n m : ℕ} (p : Fin m → MvPolynomial (Fin n) ℝ)
    (hdeg : ∀ i, (p i).totalDegree ≤ 2) :
    ∃ f : MvPolynomial (Fin n) ℝ, f.totalDegree ≤ 4 ∧
      ∀ x : Fin n → ℝ,
        (MvPolynomial.eval x f = 0 ↔ ∀ i, MvPolynomial.eval x (p i) = 0) := by sorry

end BSS

Source

L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers: NP-completeness, recursive functions and universal machines, Bull. Amer. Math. Soc. (N.S.) 21 (1989), no. 1, 1-46, https://doi.org/10.1090/S0273-0979-1989-15750-9, §4, p. 20, Proposition 1(b)

Read-back

What the Lean code literally says, in plain math · NON-BLIND: written by the drafting agent (Aristotle, Harmonic), not an independent auditor

⚠️ NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was not written by an independent blind auditor. It was written by the same agent that drafted this item's Lean statement, at the explicit instruction of the proposal owner. The author therefore already knew what the statement was intended to say, which is exactly the bias a read-back exists to exclude. Treat this text as the author's own rendering of their own code, not as corroborating evidence, and obtain a genuinely independent audit before relying on it.

Fix natural numbers $n$ and $m$ and a family $p_0, \dots, p_{m-1}$ of polynomials in $n$ variables over $\mathbb{R}$ , and assume each $p_i$ has total degree at most $2$ .

The claim asserts the existence of a single polynomial $f$ in the same $n$ variables over $\mathbb{R}$ such that $f$ has total degree at most $4$ , and such that for every point $x \in \mathbb{R}^n$ ,

f(x) = 0 \iff p_i(x) = 0 \text{ for every } i < m.

The equivalence is a genuine biconditional at every point, not merely an equality of the two solution sets stated one way round. The number of variables is not enlarged: $f$ is a polynomial in the same $n$ variables as the $p_i$ . Degenerate cases are included: $m = 0$ makes the right-hand side vacuously true, so $f$ must vanish identically on $\mathbb{R}^n$ ; and $n = 0$ makes $\mathbb{R}^n$ a single point. The hypothesis that each $p_i$ has total degree at most $2$ is assumed, not concluded.

View graph

§4 Prop. 1(b): a quadratic system is equivalent to one equation of degree ≤4\le 4≤4

§4 Prop. 1(b): a quadratic system is equivalent to one equation of degree $\le 4$