6. The Weil-pairing route to positivity🔗

Theorem6.1

uses 0used by 1✓L∃∀N

(Determinant = degree on E[\ell] — Silverman III.8.6.) For an endomorphism \psi whose Weil pairing scales by its degree, e_\ell(\psi S,\psi T)=e_\ell(S,T)^{\deg\psi}, the matrix \rho_\ell(\psi) of \psi on the \ell-torsion satisfies \det \rho_\ell(\psi) \;\equiv\; \deg\psi \pmod{\ell}. The discrete log of the symplectic Weil pairing gives an alternating bilinear form whose top exterior power reads off the determinant.

Lean code for Theorem6.1●2 theorems

theoremdefined in HasseWeil/WeilPairing/DetDeg.lean

complete

theorem HasseWeil.WeilPairing.TorsionGeometric.det_rhoEll_eq_degree.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [IsIntegrallyClosed { toAffine := W.toAffine }.CoordinateRing] (ℓ : ℕ)
  [hℓ : Fact (Nat.Prime ℓ)] [IsAlgClosed F] (hℓF : ↑ℓ ≠ 0)
  (ψ : W.toAffine.Point →+ W.toAffine.Point) (d : ℕ)
  (hsc :
    ∀ (S T : ↥(HasseWeil.torsionSubgroup W.toAffine ↑ℓ)),
      HasseWeil.WeilPairing.weilPairing W ↑ℓ ⋯ (ψ ↑S) (ψ ↑T) ⋯ ⋯ =
        HasseWeil.WeilPairing.weilPairing W ↑ℓ ⋯ ↑S ↑T ⋯ ⋯ ^ d) :
  (HasseWeil.WeilPairing.TorsionGeometric.rhoEll W ℓ hℓF ψ).det = ↑d

theorem HasseWeil.WeilPairing.TorsionGeometric.det_rhoEll_eq_degree.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  (W : WeierstrassCurve F)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [IsIntegrallyClosed
      {
          toAffine :=
            W.toAffine }.CoordinateRing]
  (ℓ : ℕ) [hℓ : Fact (Nat.Prime ℓ)]
  [IsAlgClosed F] (hℓF : ↑ℓ ≠ 0)
  (ψ :
    W.toAffine.Point →+ W.toAffine.Point)
  (d : ℕ)
  (hsc :
    ∀
      (S T :
        ↥(HasseWeil.torsionSubgroup
            W.toAffine ↑ℓ)),
      HasseWeil.WeilPairing.weilPairing W
          ↑ℓ ⋯ (ψ ↑S) (ψ ↑T) ⋯ ⋯ =
        HasseWeil.WeilPairing.weilPairing
            W ↑ℓ ⋯ ↑S ↑T ⋯ ⋯ ^
          d) :
  (HasseWeil.WeilPairing.TorsionGeometric.rhoEll
        W ℓ hℓF ψ).det =
    ↑d

**DET-DEG (matrix form)** (Silverman III.8.6): `det(ρ_ℓ ψ) = (d : ZMod ℓ)` from the pairing
scaling, via `rhoEll_det`.

theoremdefined in HasseWeil/WeilPairing/DetDeg.lean

complete

theorem HasseWeil.WeilPairing.TorsionGeometric.linearMap_det_torsionRestrict_eq.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [IsIntegrallyClosed { toAffine := W.toAffine }.CoordinateRing] (ℓ : ℕ)
  [hℓ : Fact (Nat.Prime ℓ)] [IsAlgClosed F] (hℓF : ↑ℓ ≠ 0)
  (ψ : W.toAffine.Point →+ W.toAffine.Point) (d : ℕ)
  (hsc :
    ∀ (S T : ↥(HasseWeil.torsionSubgroup W.toAffine ↑ℓ)),
      HasseWeil.WeilPairing.weilPairing W ↑ℓ ⋯ (ψ ↑S) (ψ ↑T) ⋯ ⋯ =
        HasseWeil.WeilPairing.weilPairing W ↑ℓ ⋯ ↑S ↑T ⋯ ⋯ ^ d) :
  LinearMap.det
      (HasseWeil.WeilPairing.TorsionGeometric.torsionRestrict W ℓ ψ) =
    ↑d

theorem HasseWeil.WeilPairing.TorsionGeometric.linearMap_det_torsionRestrict_eq.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  (W : WeierstrassCurve F)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [IsIntegrallyClosed
      {
          toAffine :=
            W.toAffine }.CoordinateRing]
  (ℓ : ℕ) [hℓ : Fact (Nat.Prime ℓ)]
  [IsAlgClosed F] (hℓF : ↑ℓ ≠ 0)
  (ψ :
    W.toAffine.Point →+ W.toAffine.Point)
  (d : ℕ)
  (hsc :
    ∀
      (S T :
        ↥(HasseWeil.torsionSubgroup
            W.toAffine ↑ℓ)),
      HasseWeil.WeilPairing.weilPairing W
          ↑ℓ ⋯ (ψ ↑S) (ψ ↑T) ⋯ ⋯ =
        HasseWeil.WeilPairing.weilPairing
            W ↑ℓ ⋯ ↑S ↑T ⋯ ⋯ ^
          d) :
  LinearMap.det
      (HasseWeil.WeilPairing.TorsionGeometric.torsionRestrict
        W ℓ ψ) =
    ↑d

**DET-DEG (module form)** (Silverman III.8.6): for an `AddMonoidHom ψ` preserving `E[ℓ]` whose
Weil-pairing scaling is `e_ℓ(ψS, ψT) = e_ℓ(S,T)^d`, the determinant of `ψ` on `E[ℓ]` is
`(d:ZMod ℓ)`.
Combines `omegaForm_scaling` (the additive scaling) with `PairingDet.det_eq_of_alternating_scaling`
(the `Λ²` lemma on the nondegenerate alternating form `ω`).

Proof for Theorem 6.1

uses 0

Passing to the additive form \omega = \log e_\ell makes the scaling \omega(\psi S,\psi T) = \deg\psi \cdot \omega(S,T); on the 2-dimensional symplectic space E[\ell] the induced map on \Lambda^2 is multiplication by \det\rho_\ell(\psi), forcing \det\rho_\ell(\psi) \equiv \deg\psi.

Theorem6.2

uses 0used by 1✓L∃∀N

(Frobenius determinant data on E[\ell].) For each prime \ell \ne p, the Frobenius matrix M=\rho_\ell(\pi) over \overline{K} satisfies, modulo \ell, \det M = q, \qquad \det(I-M) = q+1-t, \qquad \det(rM - sI) = \deg(r\pi-s), assembling the determinant-degree identity across the separable pencil (Silverman III.8.6

V.2.3.1).

Lean code for Theorem6.2●2 theorems

theoremdefined in HasseWeil/WeilPairing/DetDeg.lean

complete

theorem HasseWeil.WeilPairing.TorsionGeometric.frob_det_residual_of_weil_scaling.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [IsIntegrallyClosed { toAffine := W.toAffine }.CoordinateRing] (ℓ : ℕ)
  [hℓ : Fact (Nat.Prime ℓ)] [IsAlgClosed F] (hℓF : ↑ℓ ≠ 0)
  (πhom : W.toAffine.Point →+ W.toAffine.Point) (q t Dν r s : ℤ)
  (dπ d1 drs : ℕ) (hqd : ↑dπ = q) (h1d : ↑d1 = q + 1 - t)
  (hDd : ↑drs = Dν)
  (hπ :
    HasseWeil.WeilPairing.TorsionGeometric.WeilScales W ℓ hℓF πhom dπ)
  (h1 :
    HasseWeil.WeilPairing.TorsionGeometric.WeilScales W ℓ hℓF
      (AddMonoidHom.id W.toAffine.Point - πhom) d1)
  (hrs :
    HasseWeil.WeilPairing.TorsionGeometric.WeilScales W ℓ hℓF
      (r • πhom - s • AddMonoidHom.id W.toAffine.Point) drs) :
  ∃ M,
    M.det = ↑q ∧
      (1 - M).det = ↑(q + 1 - t) ∧ (↑r • M - ↑s • 1).det = ↑Dν

theorem HasseWeil.WeilPairing.TorsionGeometric.frob_det_residual_of_weil_scaling.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  (W : WeierstrassCurve F)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [IsIntegrallyClosed
      {
          toAffine :=
            W.toAffine }.CoordinateRing]
  (ℓ : ℕ) [hℓ : Fact (Nat.Prime ℓ)]
  [IsAlgClosed F] (hℓF : ↑ℓ ≠ 0)
  (πhom :
    W.toAffine.Point →+ W.toAffine.Point)
  (q t Dν r s : ℤ) (dπ d1 drs : ℕ)
  (hqd : ↑dπ = q) (h1d : ↑d1 = q + 1 - t)
  (hDd : ↑drs = Dν)
  (hπ :
    HasseWeil.WeilPairing.TorsionGeometric.WeilScales
      W ℓ hℓF πhom dπ)
  (h1 :
    HasseWeil.WeilPairing.TorsionGeometric.WeilScales
      W ℓ hℓF
      (AddMonoidHom.id W.toAffine.Point -
        πhom)
      d1)
  (hrs :
    HasseWeil.WeilPairing.TorsionGeometric.WeilScales
      W ℓ hℓF
      (r • πhom -
        s •
          AddMonoidHom.id
            W.toAffine.Point)
      drs) :
  ∃ M,
    M.det = ↑q ∧
      (1 - M).det = ↑(q + 1 - t) ∧
        (↑r • M - ↑s • 1).det = ↑Dν

**The per-`ℓ` Frobenius determinant residual from the Weil scalings, integer form** (the exact
shape of the shipped `Reduction.deg_eq_of_frob_det_data` /
`Assembly.qf_nonneg_of_frob_det_residual` hypothesis).  Given the Frobenius hom on `E[ℓ]` over `K̄`,
integers `q, t, Dν` equal (as integers) to the geometric degrees `deg π`, `q+1−deg(1−π)`,
`deg(rπ−s)`, and the three Weil-pairing scalings, there is a matrix `M = ρ_ℓ(π)` with `det M = q`,
`det(1−M) = q+1−t`, `det(rM−sI) = Dν` in `ZMod ℓ`.

theoremdefined in HasseWeil/WeilPairing/FrobMatrixData.lean

complete

theorem HasseWeil.WeilPairing.frob_det_residual_baseChange.{u_1, u_2}
  {K : Type u_1} [Field K] [Fintype K] [DecidableEq K]
  (W : WeierstrassCurve K) [WeierstrassCurve.IsElliptic W.toAffine]
  (p r : ℕ) [Fact (Nat.Prime p)] [CharP K p]
  [Fact (Fintype.card K = p ^ r)] (L : Type u_2) [Field L]
  [DecidableEq L] [Algebra K L] [IsAlgClosed L] [ExpChar L p]
  [WeierstrassCurve.IsElliptic (W.baseChange L).toAffine]
  (hq : 2 ≤ Fintype.card K) (deg : ℤ → ℤ → ℤ)
  (hdeg_nonneg : ∀ (r s : ℤ), 0 ≤ deg r s) (r' s' : ℤ) (ℓ : ℕ)
  (hℓp : Nat.Prime ℓ) (hℓF : ↑ℓ ≠ 0)
  (hsc :
    HasseWeil.WeilPairing.TorsionGeometric.WeilScales (W.baseChange L) ℓ
        hℓF (HasseWeil.WeilPairing.frobeniusHomBaseChange W p r L)
        (Fintype.card K) ∧
      HasseWeil.WeilPairing.TorsionGeometric.WeilScales (W.baseChange L)
          ℓ hℓF
          (AddMonoidHom.id (W.baseChange L).toAffine.Point -
            HasseWeil.WeilPairing.frobeniusHomBaseChange W p r L)
          (HasseWeil.isogOneSub_negFrobenius W hq).degree ∧
        HasseWeil.WeilPairing.TorsionGeometric.WeilScales
          (W.baseChange L) ℓ hℓF
          (r' • HasseWeil.WeilPairing.frobeniusHomBaseChange W p r L -
            s' • AddMonoidHom.id (W.baseChange L).toAffine.Point)
          (deg r' s').toNat) :
  ∃ M,
    M.det = ↑↑(Fintype.card K) ∧
      (1 - M).det =
          ↑(↑(Fintype.card K) + 1 -
              HasseWeil.isogTrace (HasseWeil.frobeniusIsog W)
                (HasseWeil.isogOneSub_negFrobenius W hq)) ∧
        (↑r' • M - ↑s' • 1).det = ↑(deg r' s')

theorem HasseWeil.WeilPairing.frob_det_residual_baseChange.{u_1,
    u_2}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  (p r : ℕ) [Fact (Nat.Prime p)]
  [CharP K p]
  [Fact (Fintype.card K = p ^ r)]
  (L : Type u_2) [Field L] [DecidableEq L]
  [Algebra K L] [IsAlgClosed L]
  [ExpChar L p]
  [WeierstrassCurve.IsElliptic
      (W.baseChange L).toAffine]
  (hq : 2 ≤ Fintype.card K)
  (deg : ℤ → ℤ → ℤ)
  (hdeg_nonneg : ∀ (r s : ℤ), 0 ≤ deg r s)
  (r' s' : ℤ) (ℓ : ℕ) (hℓp : Nat.Prime ℓ)
  (hℓF : ↑ℓ ≠ 0)
  (hsc :
    HasseWeil.WeilPairing.TorsionGeometric.WeilScales
        (W.baseChange L) ℓ hℓF
        (HasseWeil.WeilPairing.frobeniusHomBaseChange
          W p r L)
        (Fintype.card K) ∧
      HasseWeil.WeilPairing.TorsionGeometric.WeilScales
          (W.baseChange L) ℓ hℓF
          (AddMonoidHom.id
              (W.baseChange
                    L).toAffine.Point -
            HasseWeil.WeilPairing.frobeniusHomBaseChange
              W p r L)
          (HasseWeil.isogOneSub_negFrobenius
              W hq).degree ∧
        HasseWeil.WeilPairing.TorsionGeometric.WeilScales
          (W.baseChange L) ℓ hℓF
          (r' •
              HasseWeil.WeilPairing.frobeniusHomBaseChange
                W p r L -
            s' •
              AddMonoidHom.id
                (W.baseChange
                      L).toAffine.Point)
          (deg r' s').toNat) :
  ∃ M,
    M.det = ↑↑(Fintype.card K) ∧
      (1 - M).det =
          ↑(↑(Fintype.card K) + 1 -
              HasseWeil.isogTrace
                (HasseWeil.frobeniusIsog
                  W)
                (HasseWeil.isogOneSub_negFrobenius
                  W hq)) ∧
        (↑r' • M - ↑s' • 1).det =
          ↑(deg r' s')

Proof for Theorem 6.2

Proof uses 3

Proof dependency previews

Preview

Definition 1.6

Loading preview

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

Apply the determinant-=-degree identity (Theorem 6.1) to \pi, 1-\pi, and the separable pencil r\pi-s, then expand the 2\times2 determinants (Theorem 5.4); \deg\pi=q (Definition 1.6) and \det(I-M)=q+1-t recovers the trace.

Theorem6.3

uses 0used by 1✓L∃∀N

(Positivity of the form, via the Weil pairing.) From the per-\ell Frobenius determinant data, the Hasse quadratic form is non-negative for all (r,s): q\,r^2 - t\,rs + s^2 \;\ge\; 0. This discharges the geometric leaf without the characteristic-p dual-additivity wall, using only the separable (genuine) locus.

Lean code for Theorem6.3●2 theorems

theoremdefined in HasseWeil/WeilPairing/HasseAssembly.lean

complete

theorem HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data.{u_1}
  {K : Type u_1} [Field K] [Fintype K] [DecidableEq K]
  (W : WeierstrassCurve K) [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point] (hq : 2 ≤ Fintype.card K) (deg : ℤ → ℤ → ℤ)
  (hdeg_nonneg : ∀ (r s : ℤ), 0 ≤ deg r s)
  (hres :
    ∀ (r s : ℤ),
      ¬↑(ringChar K) ∣ s →
        ∀ (ℓ : ℕ),
          Nat.Prime ℓ →
            ℓ ≠ ringChar K →
              ∃ M,
                M.det = ↑↑(Fintype.card K) ∧
                  (1 - M).det =
                      ↑(↑(Fintype.card K) + 1 -
                          HasseWeil.isogTrace
                            (HasseWeil.frobeniusIsog W)
                            (HasseWeil.isogOneSub_negFrobenius W hq)) ∧
                    (↑r • M - ↑s • 1).det = ↑(deg r s))
  (r s : ℤ) :
  0 ≤
    ↑(Fintype.card K) * r ^ 2 -
        HasseWeil.isogTrace (HasseWeil.frobeniusIsog W)
              (HasseWeil.isogOneSub_negFrobenius W hq) *
            r *
          s +
      s ^ 2

theorem HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point]
  (hq : 2 ≤ Fintype.card K)
  (deg : ℤ → ℤ → ℤ)
  (hdeg_nonneg : ∀ (r s : ℤ), 0 ≤ deg r s)
  (hres :
    ∀ (r s : ℤ),
      ¬↑(ringChar K) ∣ s →
        ∀ (ℓ : ℕ),
          Nat.Prime ℓ →
            ℓ ≠ ringChar K →
              ∃ M,
                M.det =
                    ↑↑(Fintype.card K) ∧
                  (1 - M).det =
                      ↑(↑(Fintype.card
                                K) +
                            1 -
                          HasseWeil.isogTrace
                            (HasseWeil.frobeniusIsog
                              W)
                            (HasseWeil.isogOneSub_negFrobenius
                              W hq)) ∧
                    (↑r • M -
                          ↑s • 1).det =
                      ↑(deg r s))
  (r s : ℤ) :
  0 ≤
    ↑(Fintype.card K) * r ^ 2 -
        HasseWeil.isogTrace
              (HasseWeil.frobeniusIsog W)
              (HasseWeil.isogOneSub_negFrobenius
                W hq) *
            r *
          s +
      s ^ 2

**GAP-QF top leaf via the Weil pairing** (Silverman III.6.3 / V.2.3.1, the Route-2A capstone).

Given the per-`ℓ` Frobenius-matrix determinant data `hres` (the output of the Weil-pairing
`DET-DEG`, `det(ρ_ℓ φ) = deg φ`, for `φ ∈ {π, 1−π, rπ−s}`, on the base change of `E` to `K̄`) and a
non-negative degree function `deg` realising the third determinant, the Hasse quadratic form
`(#K)·r² − tr(π)·rs + s²` is non-negative for **all** `(r,s)` — exactly the conclusion the
legacy `qf_nonneg_skeleton` chain targeted (retired 2026-06-11).

This is the additivity-free Weil-pairing route to the GAP-QF leaf: the determinant data avoids the
characteristic-`p` dual-additivity wall (the retired `genuineIsogSmulSub_degree_eq_signed`), because the
per-isogeny scaling `det(ρ_ℓ φ) = deg φ` holds for every `φ` individually (Silverman III.8.6). It
composes `det = deg` (`DetDeg`) with the shipped arithmetic reduction
`qf_nonneg_of_frob_det_residual`.

theoremdefined in HasseWeil/WeilPairing/HasseAssembly.lean

complete

theorem HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data_both.{u_1}
  {K : Type u_1} [Field K] [Fintype K] [DecidableEq K]
  (W : WeierstrassCurve K) [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point] (hq : 2 ≤ Fintype.card K) (deg : ℤ → ℤ → ℤ)
  (hdeg_nonneg : ∀ (r s : ℤ), 0 ≤ deg r s)
  (hres :
    ∀ (r s : ℤ),
      ¬↑(ringChar K) ∣ r →
        ¬↑(ringChar K) ∣ s →
          ∀ (ℓ : ℕ),
            Nat.Prime ℓ →
              ℓ ≠ ringChar K →
                ∃ M,
                  M.det = ↑↑(Fintype.card K) ∧
                    (1 - M).det =
                        ↑(↑(Fintype.card K) + 1 -
                            HasseWeil.isogTrace
                              (HasseWeil.frobeniusIsog W)
                              (HasseWeil.isogOneSub_negFrobenius W
                                hq)) ∧
                      (↑r • M - ↑s • 1).det = ↑(deg r s))
  (r s : ℤ) :
  0 ≤
    ↑(Fintype.card K) * r ^ 2 -
        HasseWeil.isogTrace (HasseWeil.frobeniusIsog W)
              (HasseWeil.isogOneSub_negFrobenius W hq) *
            r *
          s +
      s ^ 2

theorem HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data_both.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point]
  (hq : 2 ≤ Fintype.card K)
  (deg : ℤ → ℤ → ℤ)
  (hdeg_nonneg : ∀ (r s : ℤ), 0 ≤ deg r s)
  (hres :
    ∀ (r s : ℤ),
      ¬↑(ringChar K) ∣ r →
        ¬↑(ringChar K) ∣ s →
          ∀ (ℓ : ℕ),
            Nat.Prime ℓ →
              ℓ ≠ ringChar K →
                ∃ M,
                  M.det =
                      ↑↑(Fintype.card K) ∧
                    (1 - M).det =
                        ↑(↑(Fintype.card
                                  K) +
                              1 -
                            HasseWeil.isogTrace
                              (HasseWeil.frobeniusIsog
                                W)
                              (HasseWeil.isogOneSub_negFrobenius
                                W hq)) ∧
                      (↑r • M -
                            ↑s • 1).det =
                        ↑(deg r s))
  (r s : ℤ) :
  0 ≤
    ↑(Fintype.card K) * r ^ 2 -
        HasseWeil.isogTrace
              (HasseWeil.frobeniusIsog W)
              (HasseWeil.isogOneSub_negFrobenius
                W hq) *
            r *
          s +
      s ^ 2

**GAP-QF top leaf via the Weil pairing, coprime-BOTH form** (reviewer round-23, Route B).

Identical to `qf_nonneg_skeleton_of_weil_det_data` but requesting the per-`ℓ` Frobenius det data only
on the locus `{p ∤ r ∧ p ∤ s}` (both coordinates coprime to `p = char K`).  This is exactly the locus
on which the Weil-pairing pencil scaling for `rπ − s` is available **without** the inseparable
`p ∣ r` geometric input (the last pencil `sorry`).  The discriminant lift is the stronger
`qf_nonneg_of_frob_det_residual_both`.

Proof for Theorem 6.3

Proof uses 2

Proof dependency previews

Preview

Theorem 5.3

Loading preview

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

On the separable locus \det(rM-sI) = \deg(r\pi-s) \ge 0 reduces the form modulo every \ell \ne p to a degree (Theorem 6.2); since this holds for infinitely many \ell the integer form is \ge 0 on the genuine locus, and the discriminant lemma (Theorem 5.3) extends it to all (r,s).