Non-negativity of a binary quadratic form and its discriminant

Mathlib's discrim_le_zero shows that a quadratic polynomial over a linearly ordered field which is non-negative at every point of the field has non-positive discriminant. This file supplies two facts about the homogeneous two-variable form a * x ^ 2 + b * x * y + c * y ^ 2 that it does not give: the reverse implication, and an integral version whose hypothesis is much weaker. It also records two elementary facts about discriminants used for positive definite integral forms: a negative discriminant together with 0 ≤ a forces 0 < a, and an integral discriminant is 0 or 1 modulo 4.

The integral version is the substantial one, and it is worth being precise about what makes it substantial. Over a field, non-negativity along a single line y = y₀ ≠ 0 already forces discrim a b c ≤ 0: the restriction is a quadratic in x, so discrim_le_zero applies and the resulting y₀ ^ 2 * discrim a b c ≤ 0 may be divided by y₀ ^ 2. Over ℤ the same hypothesis with x ranging over the integers is strictly weaker, and is genuinely not enough: the map x ↦ x ^ 2 - x is non-negative at every integer, yet discrim 1 (-1) 0 = 1 > 0, which is forall_int_nonneg_and_discrim_pos below. Int.discrim_le_zero_of_nonneg_of_lt_abs says that one extra condition — that |y₀| exceed the leading coefficient — repairs this, with no further quantification needed.

Together with the reverse implication this gives the upgrade that motivates the file: a form known to be non-negative only on some sparse subset of ℤ ⨯ ℤ — the locus where a fixed prime divides neither coordinate, which is all that the degree form on an elliptic curve is directly known to satisfy — is non-negative everywhere. Int.discrim_le_zero_of_nonneg_of_not_dvd_of_not_dvd pins the discriminant from that locus alone, and nonneg_of_discrim_le_zero then propagates the conclusion to every (x, y).

Main results

• nonneg_of_discrim_le_zero: 0 < a and discrim a b c ≤ 0 give 0 ≤ a x² + b x y + c y².
• Int.discrim_le_zero_of_nonneg_of_lt_abs: for a < |y|, and with no sign condition on a, non-negativity of a x² + b x y + c y² in x alone forces discrim a b c ≤ 0.
• Int.discrim_le_zero_of_nonneg_of_not_dvd_of_not_dvd: the same conclusion from non-negativity on {(x, y) : d ∤ x ∧ d ∤ y}, for any non-unit d.
• pos_of_nonneg_of_discrim_lt_zero: a quadratic of negative discriminant with 0 ≤ a has 0 < a.
• Int.discrim_emod_four: discrim a b c % 4 = b % 2, so an integral discriminant is 0 or 1 modulo 4.

The two Int.discrim_le_zero_… results are proved from a common lemma in which x runs over an arithmetic progression rather than all of ℤ. Only one x is ever used — the member of the progression nearest the minimum of the restricted form — so thinning the line to gap m costs exactly a factor m in the height hypothesis, which the choice of y absorbs; m = 1 is the full line.

The weaker hypothesis constraining only y is not stated separately: it is strictly stronger than the one above, so a caller holding it applies the same theorem through fun x y _ hy => h x y hy.

Provenance

Ported from the AINTLIB HasseWeil project (Apache-2.0), revision 513e83879e2f, file HasseWeil/WeilPairing/Discriminant.lean, declarations exists_int_balanced, qf_nonneg_of_nonneg_on_coprime and qf_nonneg_of_nonneg_on_coprime_both. The statements here are strictly stronger: the form is arbitrary rather than q r² − t r s + s², no primality is assumed, and a single y replaces an infinite family of prime powers.

The source proves its two locus results independently, the d ∤ y one by an infinite family of prime powers together with a balanced-remainder lemma. Neither is reproduced. The d ∤ y statement is not carried at all: it follows from the d ∤ x ∧ d ∤ y one in a line, its hypothesis being the stronger of the two. The balanced remainder it needed is Mathlib's round.

References

• Silverman, The Arithmetic of Elliptic Curves, V.1.2 — the Cauchy–Schwarz step that turns positivity of the degree form on a rank-two lattice into the Hasse inequality of V.1.1.

theorem nonneg_of_discrim_le_zero {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a b c : R} (ha : 0 < a) (hd : discrim a b c ≤ 0) (x y : R) : 0 ≤ a * x ^ 2 + b * x * y + c * y ^ 2

A binary quadratic form with positive leading coefficient and non-positive discriminant is non-negative. This is the implication opposite to Mathlib's discrim_le_zero, stated for the homogeneous two-variable form and over a linearly ordered commutative ring rather than a field. The hypothesis 0 < a cannot be dropped: discrim 0 0 (-1) = 0, while - y ^ 2 is negative.

theorem pos_of_nonneg_of_discrim_lt_zero {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a b c : R} (ha : 0 ≤ a) (hd : discrim a b c < 0) : 0 < a

A quadratic of negative discriminant with a non-negative leading coefficient has a positive one: at a = 0 the discriminant is b ^ 2, which is not negative.

theorem Int.discrim_le_zero_of_nonneg_of_lt_abs {a b c y : ℤ} (hy : a < |y|) (h : ∀ (x : ℤ), 0 ≤ a * x ^ 2 + b * x * y + c * y ^ 2) : discrim a b c ≤ 0

A single line of large enough height pins the discriminant. If a binary quadratic form over ℤ is non-negative at (x, y) for a fixed y with a < |y| and every integer x, then discrim a b c ≤ 0, that is b ^ 2 ≤ 4 * a * c.

No sign hypothesis on a is needed. A negative leading coefficient makes the hypothesis unsatisfiable, and a zero one collapses the form to a linear function of x, forcing b = 0.

The height hypothesis a < |y| is necessary, not an artefact of the proof: without it the integer-valued hypothesis is strictly weaker than its field counterpart, as forall_int_nonneg_and_discrim_pos witnesses.

theorem Int.discrim_le_zero_of_nonneg_of_not_dvd_of_not_dvd {a b c d : ℤ} (hd : ¬IsUnit d) (h : ∀ (x y : ℤ), ¬d ∣ x → ¬d ∣ y → 0 ≤ a * x ^ 2 + b * x * y + c * y ^ 2) : discrim a b c ≤ 0

The locus where d divides neither coordinate pins the discriminant. If a binary quadratic form over ℤ is non-negative at every (x, y) with d ∤ x and d ∤ y, for a non-unit d, then discrim a b c ≤ 0.

The one-coordinate variant, constraining only y, is not stated separately: its hypothesis holds on a strictly larger set of points, so it is the stronger of the two and a caller holding it applies this theorem through fun x y _ hy => h x y hy. The implication does not run the other way, and it is this form that an elliptic curve supplies, the pencil r π − s being known to be an isogeny only away from both coordinates.

d = 0 is allowed, the hypothesis then being non-negativity at every (x, y) with x ≠ 0 and y ≠ 0.

@[simp]

theorem Int.discrim_emod_four (a b c : ℤ) : discrim a b c % 4 = b % 2

The discriminant b² - 4 a c of integers a, b, c leaves the remainder b % 2 on division by 4, so it is 0 or 1 modulo 4.