15 and 290 theorems

DefinitionQuadratic form of an integer matrix#✓fully proved

For an \(n \times n\) matrix \(Q\) with integer entries, the quadratic form of \(Q\) is the map \(\mathbb{Z}^n \to \mathbb{Z}\) sending \(x\) to \(Q(x) = \sum_{i,j} Q_{ij} x_i x_j\), where \(i\) and \(j\) range over \(\{0, \dots, n-1\}\). No symmetry of \(Q\) is assumed.

def evalQ {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℤ) (x : Fin n → ℤ) : ℤ :=
  ∑ i, ∑ j, Q i j * x i * x j

Used by 1

Used byIntegers represented by an integer-matrix quadratic form

DefinitionIntegers represented by an integer-matrix quadratic form#✓fully proved

An \(n \times n\) matrix \(Q\) with integer entries represents an integer \(m\) if \(Q(x) = m\) for some \(x \in \mathbb{Z}^n\), where \(Q(x) = \sum_{i,j} Q_{ij} x_i x_j\).

def Represents {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℤ) (m : ℤ) : Prop :=
  ∃ x : Fin n → ℤ, evalQ Q x = m

Uses 1 · Used by 2

Statement usesQuadratic form of an integer matrix

Used byConway–Schneeberger fifteen theorem · Universal integer-matrix quadratic forms

DefinitionUniversal integer-matrix quadratic forms#✓fully proved

An \(n \times n\) matrix \(Q\) with integer entries is universal if its quadratic form \(Q(x) = \sum_{i,j} Q_{ij} x_i x_j\) represents every positive integer, that is, for every positive integer \(m\) there is \(x \in \mathbb{Z}^n\) with \(Q(x) = m\).

def IsUniversal {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℤ) : Prop :=
  ∀ m : ℕ, 0 < m → Represents Q (m : ℤ)

Uses 1 · Used by 1

Statement usesIntegers represented by an integer-matrix quadratic form

Used byConway–Schneeberger fifteen theorem

TheoremConway–Schneeberger fifteen theorem#●ready to prove

Let \(Q\) be a positive definite symmetric \(n \times n\) matrix with integer entries, with quadratic form \(Q(x) = \sum_{i,j} Q_{ij} x_i x_j\) on \(\mathbb{Z}^n\). Then \(Q\) is universal, that is, it represents every positive integer, if and only if it represents every integer \(k\) with \(1 \le k \le 15\).

The forward direction is immediate; the content is the converse. Bhargava's refinement reduces the critical set to \(\{1, 2, 3, 5, 6, 7, 10, 14, 15\}\).

public theorem_wanted conway_schneeberger_fifteen {n : ℕ}
    (Q : Matrix (Fin n) (Fin n) ℤ)
    (_hpos : Q.PosDef) :
    IsUniversal Q ↔ ∀ k ∈ Finset.Icc (1 : ℤ) 15, Represents Q k

Sources

• Conway–Schneeberger 1993 (unpublished, communicated by Conway in lectures); full proof M. Bhargava, 'On the Conway–Schneeberger fifteen theorem', in Quadratic Forms and their Applications (Contemp. Math. 272, AMS 2000). Listed as §95 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem conway_schneeberger_fifteen of the lean-eval benchmark.

Uses 2

Statement usesUniversal integer-matrix quadratic forms · Integers represented by an integer-matrix quadratic form

DefinitionQuadratic form of a matrix#✓fully proved

For a ring \(R\) and an \(n \times n\) matrix \(M\) with entries in \(R\), the value of the quadratic form of \(M\) at a vector \(x \in R^n\) is \(x \cdot (M x) = \sum_{i,j} x_i M_{ij} x_j\), where \(i\) and \(j\) range over \(\{0, \dots, n-1\}\).

No symmetry of \(M\) is assumed, and \(R\) need not be commutative.

def evalQ (M : Matrix (Fin n) (Fin n) R) (v : Fin n → R) : R := v ⬝ᵥ M *ᵥ v

Used by 2

Used byInteger-valued quadratic forms · Natural numbers represented by a quadratic form

DefinitionNatural numbers represented by a quadratic form#✓fully proved

For a ring \(R\), an \(n \times n\) matrix \(M\) with entries in \(R\) represents a natural number \(m\) if there is an integer vector \(x \in \mathbb{Z}^n\) with \(\sum_{i,j} x_i M_{ij} x_j = m\), where the entries of \(x\) and the number \(m\) are viewed as elements of \(R\).

def Represents (M : Matrix (Fin n) (Fin n) R) (m : ℕ) : Prop :=
  ∃ v : Fin n → ℤ, evalQ M (v · : _ → R) = m

Uses 1 · Used by 2

Statement usesQuadratic form of a matrix

Used byUniversal quadratic forms over a ring · The 290 theorem

DefinitionUniversal quadratic forms over a ring#✓fully proved

For a ring \(R\), an \(n \times n\) matrix \(M\) with entries in \(R\) is universal if it represents every positive integer: for every positive integer \(m\) there is \(x \in \mathbb{Z}^n\) with \(\sum_{i,j} x_i M_{ij} x_j = m\) in \(R\).

def IsUniversal (M : Matrix (Fin n) (Fin n) R) : Prop :=
  ∀ m : ℕ, 0 < m → Represents M m

Uses 1 · Used by 1

Statement usesNatural numbers represented by a quadratic form

Used byThe 290 theorem

DefinitionInteger-valued quadratic forms#✓fully proved

For a ring \(R\), an \(n \times n\) matrix \(M\) with entries in \(R\) is integral if its quadratic form takes integer values at integer vectors: for every \(x \in \mathbb{Z}^n\), the value \(\sum_{i,j} x_i M_{ij} x_j\) computed in \(R\) lies in the image of \(\mathbb{Z}\) in \(R\).

def Integral (M : Matrix (Fin n) (Fin n) R) : Prop :=
  ∀ v : Fin n → ℤ, evalQ M (v · : _ → R) ∈ Set.range ((↑) : ℤ → R)

Uses 1 · Used by 1

Statement usesQuadratic form of a matrix

Used byThe 290 theorem

DefinitionCritical numbers of the 290 theorem#✓fully proved

The critical numbers of the 290 theorem form the set of the 29 natural numbers \(1, 2, 3, 5, 6, 7, 10, 13, 14, 15, 17, 19, 21, 22, 23, 26, 29, 30, 31, 34, 35, 37, 42, 58, 93, 110, 145, 203, 290\).

def criticalNumbers : Finset ℕ :=
  {1, 2, 3, 5, 6, 7, 10, 13, 14, 15, 17, 19, 21, 22, 23, 26, 29, 30, 31,
   34, 35, 37, 42, 58, 93, 110, 145, 203, 290}

Used by 1

Used byThe 290 theorem

TheoremThe 290 theorem#●ready to prove

Let \(n\) be a natural number and let \(M\) be a real \(n \times n\) matrix that is positive definite (symmetric, with \(x^{\top} M x > 0\) for every nonzero \(x \in \mathbb{R}^n\)) and integral (for every \(x \in \mathbb{Z}^n\), the value \(x^{\top} M x\) is an integer). If \(M\) represents each of the 29 critical numbers of the 290 theorem, that is, for each critical number \(m\) there is \(x \in \mathbb{Z}^n\) with \(x^{\top} M x = m\), then \(M\) is universal: for every positive integer \(m\) there is \(x \in \mathbb{Z}^n\) with \(x^{\top} M x = m\).

public theorem_wanted two_ninety_theorem {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ)
    (hpos : M.PosDef)
    (hIntegral : Integral M)
    (hrep : ∀ m ∈ criticalNumbers, Represents M m) :
    IsUniversal M

Sources

• M. Bhargava, J. Hanke, Universal quadratic forms and the 290-theorem, preprint (2011). See also https://en.wikipedia.org/wiki/15_and_290_theorems. Problem two_ninety_theorem of the lean-eval benchmark.

Uses 4

Statement usesInteger-valued quadratic forms · Universal quadratic forms over a ring · Natural numbers represented by a quadratic form · Critical numbers of the 290 theorem

8 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.