5. The arithmetic core: discriminant of a binary quadratic form🔗

Theorem5.1

uses 0

Used by 4

Reverse dependency previews

Preview

Theorem 3.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

(Arithmetic core.) Let q be a positive integer and t \in \mathbb{Z}. If the binary form q\,r^2 - t\,r\,s + s^2 is non-negative for all integers r, s, then t^2 \;\le\; 4q.

Lean code for Theorem5.1●1 theorem

theoremdefined in HasseWeil/HasseBound.lean

complete

theorem HasseWeil.trace_sq_le_four_mul_deg (q : ℕ) (t : ℤ) (hq : 0 < q)
  (h : ∀ (r s : ℤ), 0 ≤ ↑q * r ^ 2 - t * r * s + s ^ 2) : t ^ 2 ≤ 4 * ↑q

theorem HasseWeil.trace_sq_le_four_mul_deg (q : ℕ)
  (t : ℤ) (hq : 0 < q)
  (h :
    ∀ (r s : ℤ),
      0 ≤
        ↑q * r ^ 2 - t * r * s + s ^ 2) :
  t ^ 2 ≤ 4 * ↑q

If a binary quadratic form `q · r² - t · r · s + s²` is non-negative for all
integers `r, s`, then `t² ≤ 4q`.

Proof for Theorem 5.1

uses 0

Specialise the non-negativity hypothesis at (r, s) = (t, 2q): this gives q\,t^2 - 2q\,t^2 + 4q^2 = q\,(4q - t^2) \ge 0, and since q > 0 we conclude t^2 \le 4q. (This is the discriminant-non-positivity of the binary form, made elementary by evaluating at the point where the form is minimised along the line s = 2q.)

Theorem5.2

uses 0

Used by 2

Reverse dependency previews

Preview

Theorem 7.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

(Passage to square roots.) For q \in \mathbb{N} and t \in \mathbb{Z}, if t^2 \le 4q then |t| \;\le\; 2\sqrt{q} as real numbers.

Lean code for Theorem5.2●1 theorem

theoremdefined in HasseWeil/HasseBound.lean

complete

theorem HasseWeil.abs_le_two_sqrt_of_sq_le (q : ℕ) (t : ℤ)
  (ht : t ^ 2 ≤ 4 * ↑q) : |↑t| ≤ 2 * √↑q

theorem HasseWeil.abs_le_two_sqrt_of_sq_le (q : ℕ)
  (t : ℤ) (ht : t ^ 2 ≤ 4 * ↑q) :
  |↑t| ≤ 2 * √↑q

The integer absolute value bound: if `t² ≤ 4q`, then `|t| ≤ 2√q`.

Proof for Theorem 5.2

uses 1

Over \mathbb{R}, (2\sqrt{q})^2 = 4q \ge t^2, and both |t| and 2\sqrt{q} are non-negative, so taking square roots of t^2 \le (2\sqrt{q})^2 preserves the inequality (Theorem 5.1).

Theorem5.3

uses 0used by 1✓L∃∀N

(From the genuine locus to all of \mathbb{Z}^2.) If the form q r^2 - t rs + s^2 (with q>0) is non-negative on every (r,s) coprime to the characteristic p, then it is non-negative on all (r,s). This is the discriminant lemma that lets the Weil-pairing route demand the degree identity only where r\pi-s is separable.

Lean code for Theorem5.3●2 theorems

theoremdefined in HasseWeil/WeilPairing/Discriminant.lean

complete

theorem HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime {q t : ℤ}
  (hq : 0 < q) {p : ℕ} (hp : Nat.Prime p)
  (h : ∀ (r s : ℤ), ¬↑p ∣ s → 0 ≤ q * r ^ 2 - t * r * s + s ^ 2)
  (r s : ℤ) : 0 ≤ q * r ^ 2 - t * r * s + s ^ 2

theorem HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime
  {q t : ℤ} (hq : 0 < q) {p : ℕ}
  (hp : Nat.Prime p)
  (h :
    ∀ (r s : ℤ),
      ¬↑p ∣ s →
        0 ≤ q * r ^ 2 - t * r * s + s ^ 2)
  (r s : ℤ) :
  0 ≤ q * r ^ 2 - t * r * s + s ^ 2

**The discriminant lemma (Silverman V.1.1).** If the quadratic form `Q(r,s) = q·r² − t·rs + s²`
(with `0 < q`) is non-negative on every `(r,s)` whose `s` is coprime to a prime `p`, then it is
non-negative on **all** `(r,s)`.

Step 1 forces `t² ≤ 4q` (a contradiction otherwise, via a `p`-coprime witness `s = ℓⁿ`); step 2 is
the positive-semidefiniteness `4q·Q = (2qr − ts)² + (4q − t²)s² ≥ 0`.

theoremdefined in HasseWeil/WeilPairing/Discriminant.lean

complete

theorem HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime_both {q t : ℤ}
  (hq : 0 < q) {p : ℕ} (hp : Nat.Prime p)
  (h :
    ∀ (r s : ℤ), ¬↑p ∣ r → ¬↑p ∣ s → 0 ≤ q * r ^ 2 - t * r * s + s ^ 2)
  (r s : ℤ) : 0 ≤ q * r ^ 2 - t * r * s + s ^ 2

theorem HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime_both
  {q t : ℤ} (hq : 0 < q) {p : ℕ}
  (hp : Nat.Prime p)
  (h :
    ∀ (r s : ℤ),
      ¬↑p ∣ r →
        ¬↑p ∣ s →
          0 ≤
            q * r ^ 2 - t * r * s + s ^ 2)
  (r s : ℤ) :
  0 ≤ q * r ^ 2 - t * r * s + s ^ 2

**The discriminant lemma, coprime-in-BOTH-coordinates form** (reviewer round-23, Route B).
If the quadratic form `Q(r,s) = q·r² − t·rs + s²` (with `0 < q`) is non-negative on every `(r,s)` whose
**both** coordinates are coprime to a prime `p` (`p ∤ r` and `p ∤ s`), then it is non-negative on
**all** `(r,s)`.

This weakens the hypothesis of `qf_nonneg_of_nonneg_on_coprime` (which assumes `≥ 0` on the larger
set `{p ∤ s}`) to the smaller set `{p ∤ r ∧ p ∤ s}` — exactly the locus on which the Weil-pairing
pencil scaling is available **without** the inseparable `p ∣ r'` geometric input.

Step 1 forces `t² ≤ 4q` by the reviewer's **explicit** negative witness — no density / CRT /
balanced-remainder argument: if `Δ := t² − 4q > 0`, set `C := q − t + 1`, `m := p·(|C| + 1)`,
`r := m·t + 1`, `s := 2·m·q + 1`.  Then `p ∣ m` makes `r ≡ s ≡ 1 (mod p)`, so `p ∤ r, s`, while the
`ring` identity `Q(m·t+1, 2·m·q+1) = (4q − t²)(q·m² + m) + (q − t + 1) = −Δ·(q·m² + m) + C` is
`< 0` (since `Δ·(q·m² + m) ≥ q·m² + m ≥ |C| + 1 > C`), contradicting `Q ≥ 0`.  Step 2 reuses the
positive-semidefiniteness `4q·Q = (2qr − ts)² + (4q − t²)s² ≥ 0`.

Proof for Theorem 5.3

uses 1

A coprime witness forces t^2 \le 4q (Theorem 5.1); then the positive-semidefinite completion 4q\,(q r^2 - t rs + s^2) = (2qr - ts)^2 + (4q-t^2)s^2 \ge 0 extends non-negativity to every (r,s).

Theorem5.4

uses 0used by 1✓L∃∀N

(The 2\times2 determinant is the quadratic form.) For a 2\times2 matrix M, \det(rM - sI) \;=\; r^2\det M - rs\,\operatorname{tr}M + s^2, \qquad \det(I-M) = 1 - \operatorname{tr}M + \det M. With M = \rho_\ell(\pi) the Frobenius matrix on E[\ell], the right-hand side is exactly the Hasse quadratic form modulo \ell (Silverman V.2.3.1).

Lean code for Theorem5.4●2 theorems

theoremdefined in HasseWeil/WeilPairing/MatrixDet.lean

complete

theorem HasseWeil.WeilPairing.det_smul_sub_smul_one_fin_two.{u_1} {R : Type u_1}
  [CommRing R] (M : Matrix (Fin 2) (Fin 2) R) (r s : R) :
  (r • M - s • 1).det = r ^ 2 * M.det - r * s * M.trace + s ^ 2

theorem HasseWeil.WeilPairing.det_smul_sub_smul_one_fin_two.{u_1}
  {R : Type u_1} [CommRing R]
  (M : Matrix (Fin 2) (Fin 2) R)
  (r s : R) :
  (r • M - s • 1).det =
    r ^ 2 * M.det - r * s * M.trace +
      s ^ 2

**The 2×2 determinant identity** `det(r·M − s·1) = r²·det M − r·s·tr M + s²`.

The characteristic-polynomial value of `M` at the "point" `(r,s)`, written without forming the
characteristic polynomial: a direct `det_fin_two` computation.

theoremdefined in HasseWeil/WeilPairing/MatrixDet.lean

complete

theorem HasseWeil.WeilPairing.det_one_sub_fin_two.{u_1} {R : Type u_1}
  [CommRing R] (M : Matrix (Fin 2) (Fin 2) R) :
  (1 - M).det = 1 - M.trace + M.det

theorem HasseWeil.WeilPairing.det_one_sub_fin_two.{u_1}
  {R : Type u_1} [CommRing R]
  (M : Matrix (Fin 2) (Fin 2) R) :
  (1 - M).det = 1 - M.trace + M.det

**Trace from `det(1 − M)`** (2×2): `(1 − M).det = 1 − tr M + det M`. The assembly reads the
Frobenius trace off `det(1 − π|E[ℓ]) = deg(1 − π) = #E`, giving `tr(π|E[ℓ]) = 1 + q − #E = t`.

Proof for Theorem 5.4

uses 0

Direct expansion via \det of a 2\times2 matrix; the second identity is the case r=s=1 with a sign.