conway_schneeberger_fifteen.toml

id = "conway_schneeberger_fifteen"
title = "Conway–Schneeberger fifteen theorem"
test = false
module = "LeanEval.NumberTheory.ConwaySchneebergerFifteen"
holes = ["conway_schneeberger_fifteen"]
submitter = "Kim Morrison"
notes = "A positive-definite integer-matrix quadratic form Q : ℤⁿ → ℤ is universal (represents every positive integer) iff it represents every integer in {1, 2, …, 15}. The matrix-explicit formulation records the classically integral hypothesis: the form is given by an integral symmetric matrix, so off-diagonal polynomial coefficients are even — distinguishing this 15 theorem from Bhargava–Hanke's 290 theorem (integer-valued forms, off-diagonal half-integers allowed). §95 of Knill's *Some Fundamental Theorems in Mathematics*."
source = "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)."
informal_solution = "Bhargava's proof reduces universality to representation of a 9-element critical set {1, 2, 3, 5, 6, 7, 10, 14, 15} via the *escalator-tree* argument: any non-universal positive-definite integer-matrix form has a smallest non-represented integer m, and the escalator extensions by adding diagonal m form a finite tree whose leaves can be enumerated. Exhaustive case analysis on the tree shows that any non-universal form must fail to represent at least one of the nine critical integers. Mathlib has `Nat.sum_four_squares` (Lagrange) but no universal-quadratic-form framework: no `IsUniversal` predicate, no escalator construction, no integer-matrix-versus-integer-valued distinction. The 15 in the statement is sharp: the form (1, 2, 5, 5) represents {1, …, 14} but not 15."