3. The degree quadratic form🔗

Theorem3.1

uses 0used by 0✓L∃∀N

(Degree form, scalar case — unconditional.) For the scalar endomorphism [m] and r,s \in \mathbb{Z}, \deg([\,r m - s\,]) \;=\; m^2 r^2 - 2m\,rs + s^2 \;=\; (\deg[m])\,r^2 - \operatorname{tr}([m])\,rs + s^2. This is the binary-quadratic-form identity for the degree, proved unconditionally for scalars (Silverman III.6.3).

Lean code for Theorem3.1●1 theorem

theoremdefined in HasseWeil/Endomorphism.lean

complete

theorem HasseWeil.degree_quadratic_mulByInt.{u_2} {F : Type u_2} [Field F]
  [DecidableEq F] {W : WeierstrassCurve F}
  [WeierstrassCurve.IsElliptic W.toAffine] (m r s : ℤ) (hm : m ≠ 0)
  (hm1 : 1 - m ≠ 0) (h_ne : r * m - s ≠ 0) :
  ↑(HasseWeil.isogSmulSub_mulByInt m r s).degree =
    ↑(HasseWeil.mulByInt W.toAffine m).degree * r ^ 2 -
        HasseWeil.isogTrace (HasseWeil.mulByInt W.toAffine m)
              (HasseWeil.mulByInt W.toAffine (1 - m)) *
            r *
          s +
      s ^ 2

theorem HasseWeil.degree_quadratic_mulByInt.{u_2}
  {F : Type u_2} [Field F] [DecidableEq F]
  {W : WeierstrassCurve F}
  [WeierstrassCurve.IsElliptic W.toAffine]
  (m r s : ℤ) (hm : m ≠ 0)
  (hm1 : 1 - m ≠ 0)
  (h_ne : r * m - s ≠ 0) :
  ↑(HasseWeil.isogSmulSub_mulByInt m r
          s).degree =
    ↑(HasseWeil.mulByInt W.toAffine
                m).degree *
          r ^ 2 -
        HasseWeil.isogTrace
              (HasseWeil.mulByInt
                W.toAffine m)
              (HasseWeil.mulByInt
                W.toAffine (1 - m)) *
            r *
          s +
      s ^ 2

**T-III-6-3 (unconditional mulByInt case)**: the degree quadratic
formula holds for `α = [m]`: `deg([r·m - s]) = m²r² - 2m·r·s + s²`.

Proof for Theorem 3.1

Proof uses 2

Proof dependency previews

Preview

Theorem 1.4

Loading preview

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

Substitute \deg[rm-s] = (rm-s)^2, \deg[m]=m^2, and \operatorname{tr}([m])=2m (Theorem 1.4, Theorem 2.4) and expand; both sides equal (rm-s)^2.

Theorem3.2

uses 0used by 1✓L∃∀N

(Degree form, genuine Frobenius pencil — Silverman III.6.3.) For the genuine isogeny r\pi - s (built from a dual V of \pi and the trace identity), \deg(r\pi - s) \;=\; q\,r^2 - t\,rs + s^2, \qquad t = \operatorname{tr}\pi,\ q=\deg\pi, the polarisation identity that realises the degree as a binary quadratic form on the rank-two lattice \mathbb{Z}\,1 \oplus \mathbb{Z}\,\pi.

Lean code for Theorem3.2●1 theorem

theoremdefined in HasseWeil/DegreeQuadraticForm.lean

complete

theorem HasseWeil.degree_quadratic_genuine_addIsog.{u_2} {F : Type u_2}
  [Field F] [DecidableEq F] {W : WeierstrassCurve F}
  [WeierstrassCurve.IsElliptic W.toAffine]
  (α α_dual one_sub_α : HasseWeil.Isogeny W.toAffine W.toAffine)
  (r s : ℤ)
  (hxy_β :
    HasseWeil.AddNonInversePair (HasseWeil.Isogeny.zsmul r α)
      (HasseWeil.mulByInt W.toAffine (-s)))
  (hinj_β : Function.Injective ⇑(HasseWeil.addCoordAlgHomPair hxy_β))
  (hxy_β_dual :
    HasseWeil.AddNonInversePair (HasseWeil.Isogeny.zsmul r α_dual)
      (HasseWeil.mulByInt W.toAffine (-s)))
  (hinj_β_dual :
    Function.Injective ⇑(HasseWeil.addCoordAlgHomPair hxy_β_dual))
  (h_dual_comp :
    ∀ (P : W.toAffine.Point),
      α_dual.toAddMonoidHom (α.toAddMonoidHom P) = ↑α.degree • P)
  (h_sum_trace :
    α.toAddMonoidHom + α_dual.toAddMonoidHom =
      (HasseWeil.mulByInt W.toAffine
          (HasseWeil.isogTrace α one_sub_α)).toAddMonoidHom)
  (h_deg_bridge :
    ((HasseWeil.addIsog hxy_β_dual hinj_β_dual).comp
            (HasseWeil.addIsog hxy_β hinj_β)).toAddMonoidHom =
        (HasseWeil.mulByInt W.toAffine
            (↑α.degree * r ^ 2 -
                HasseWeil.isogTrace α one_sub_α * r * s +
              s ^ 2)).toAddMonoidHom →
      ((HasseWeil.addIsog hxy_β_dual hinj_β_dual).comp
            (HasseWeil.addIsog hxy_β hinj_β)).degree =
        ((↑α.degree * r ^ 2 - HasseWeil.isogTrace α one_sub_α * r * s +
              s ^ 2) ^
            2).toNat)
  (h_dual_deg :
    (HasseWeil.addIsog hxy_β_dual hinj_β_dual).degree =
      (HasseWeil.addIsog hxy_β hinj_β).degree)
  (h_nonneg_N :
    0 ≤
      ↑α.degree * r ^ 2 - HasseWeil.isogTrace α one_sub_α * r * s +
        s ^ 2) :
  ↑(HasseWeil.addIsog hxy_β hinj_β).degree =
    ↑α.degree * r ^ 2 - HasseWeil.isogTrace α one_sub_α * r * s + s ^ 2

theorem HasseWeil.degree_quadratic_genuine_addIsog.{u_2}
  {F : Type u_2} [Field F] [DecidableEq F]
  {W : WeierstrassCurve F}
  [WeierstrassCurve.IsElliptic W.toAffine]
  (α α_dual one_sub_α :
    HasseWeil.Isogeny W.toAffine
      W.toAffine)
  (r s : ℤ)
  (hxy_β :
    HasseWeil.AddNonInversePair
      (HasseWeil.Isogeny.zsmul r α)
      (HasseWeil.mulByInt W.toAffine
        (-s)))
  (hinj_β :
    Function.Injective
      ⇑(HasseWeil.addCoordAlgHomPair
          hxy_β))
  (hxy_β_dual :
    HasseWeil.AddNonInversePair
      (HasseWeil.Isogeny.zsmul r α_dual)
      (HasseWeil.mulByInt W.toAffine
        (-s)))
  (hinj_β_dual :
    Function.Injective
      ⇑(HasseWeil.addCoordAlgHomPair
          hxy_β_dual))
  (h_dual_comp :
    ∀ (P : W.toAffine.Point),
      α_dual.toAddMonoidHom
          (α.toAddMonoidHom P) =
        ↑α.degree • P)
  (h_sum_trace :
    α.toAddMonoidHom +
        α_dual.toAddMonoidHom =
      (HasseWeil.mulByInt W.toAffine
          (HasseWeil.isogTrace α
            one_sub_α)).toAddMonoidHom)
  (h_deg_bridge :
    ((HasseWeil.addIsog hxy_β_dual
                hinj_β_dual).comp
            (HasseWeil.addIsog hxy_β
              hinj_β)).toAddMonoidHom =
        (HasseWeil.mulByInt W.toAffine
            (↑α.degree * r ^ 2 -
                HasseWeil.isogTrace α
                      one_sub_α *
                    r *
                  s +
              s ^ 2)).toAddMonoidHom →
      ((HasseWeil.addIsog hxy_β_dual
                hinj_β_dual).comp
            (HasseWeil.addIsog hxy_β
              hinj_β)).degree =
        ((↑α.degree * r ^ 2 -
                HasseWeil.isogTrace α
                      one_sub_α *
                    r *
                  s +
              s ^ 2) ^
            2).toNat)
  (h_dual_deg :
    (HasseWeil.addIsog hxy_β_dual
          hinj_β_dual).degree =
      (HasseWeil.addIsog hxy_β
          hinj_β).degree)
  (h_nonneg_N :
    0 ≤
      ↑α.degree * r ^ 2 -
          HasseWeil.isogTrace α
                one_sub_α *
              r *
            s +
        s ^ 2) :
  ↑(HasseWeil.addIsog hxy_β
          hinj_β).degree =
    ↑α.degree * r ^ 2 -
        HasseWeil.isogTrace α one_sub_α *
            r *
          s +
      s ^ 2

**Silverman III.6.3 polarisation identity, genuine `addIsog` form**: for the
genuine `r·α − s·id` isogeny `addIsog hxy_β hinj_β` (with α₁ = α.zsmul r,
α₂ = mulByInt (-s)) and a corresponding `addIsog`-built `r·α_dual − s·id`,
given the standard Silverman III.6 inputs (dual composition, sum trace,
dual-degree equality, degree bridge, QF non-negativity) the III.6.3
identity

  `(addIsog hxy_β hinj_β).degree = (α.degree)·r² − (tr α)·rs + s²`

holds at the integer level.

Drop-in form: once Worker B's D-track ships `hxy_β/hinj_β` axiom-clean (and
the analogous V-pair from Worker C), this becomes the unconditional general-α
polarisation identity, replacing the deleted false `degree_quadratic`.

Reference: Silverman, *The Arithmetic of Elliptic Curves*, Cor. III.6.3.

Proof for Theorem 3.2

Proof uses 3

Proof dependency previews

Preview

Definition 1.6

Loading preview

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

Compose r\pi - s with its dual rV - s and read off \deg(r\pi-s) from (rV-s)\circ(r\pi-s) = [\,q r^2 - t rs + s^2\,], using the dual-composition, trace-sum (Theorem 2.5), and dual-additivity (Theorem 2.2) witnesses (Definition 1.6).

Theorem3.3

uses 1used by 1✓L∃∀N

(Positivity of the degree form.) Because the degree of an isogeny is a non-negative integer, the binary form is positive semi-definite on the Frobenius pencil: q\,r^2 - t\,rs + s^2 \;=\; \deg(r\pi - s) \;\ge\; 0 \qquad \text{for all } r,s \in \mathbb{Z} (Theorem 3.2). This is the sole geometric input to the bound.

Lean code for Theorem3.3●2 theorems

theoremdefined in HasseWeil/Hasse/QuadraticForm.lean

complete

theorem HasseWeil.qf_nonneg_of_genuine_chain.{u_1} {K : Type u_1} [Field K]
  [Fintype K] [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  (β_pc : HasseWeil.Isogeny W.toAffine W.toAffine)
  (β : ℤ → ℤ → HasseWeil.Isogeny W.toAffine W.toAffine)
  (h_β_deg :
    ∀ (r s : ℤ),
      ↑(β r s).degree =
        ↑(Fintype.card K) * r ^ 2 -
            HasseWeil.isogTrace (HasseWeil.frobeniusIsog W) β_pc * r *
              s +
          s ^ 2)
  (r s : ℤ) :
  0 ≤
    ↑(Fintype.card K) * r ^ 2 -
        HasseWeil.isogTrace (HasseWeil.frobeniusIsog W) β_pc * r * s +
      s ^ 2

theorem HasseWeil.qf_nonneg_of_genuine_chain.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  (β_pc :
    HasseWeil.Isogeny W.toAffine
      W.toAffine)
  (β :
    ℤ →
      ℤ →
        HasseWeil.Isogeny W.toAffine
          W.toAffine)
  (h_β_deg :
    ∀ (r s : ℤ),
      ↑(β r s).degree =
        ↑(Fintype.card K) * r ^ 2 -
            HasseWeil.isogTrace
                  (HasseWeil.frobeniusIsog
                    W)
                  β_pc *
                r *
              s +
          s ^ 2)
  (r s : ℤ) :
  0 ≤
    ↑(Fintype.card K) * r ^ 2 -
        HasseWeil.isogTrace
              (HasseWeil.frobeniusIsog W)
              β_pc *
            r *
          s +
      s ^ 2

**`qf_nonneg` from the genuine isogeny chain** (Silverman III.6.3 + degree
non-negativity): given a genuine `β r s` family realising `r·π − s·id` at the
`AddMonoidHom` level whose degree matches the QF expression, the QF
non-negativity follows from `Int.natCast_nonneg (β r s).degree`.

theoremdefined in HasseWeil/Endomorphism.lean

complete

theorem HasseWeil.degree_quadratic_mulByInt_nonneg.{u_2} {F : Type u_2}
  [Field F] [DecidableEq F] {W : WeierstrassCurve F}
  [WeierstrassCurve.IsElliptic W.toAffine] (m r s : ℤ) (hm : m ≠ 0)
  (hm1 : 1 - m ≠ 0) (h_ne : r * m - s ≠ 0) :
  0 ≤
    ↑(HasseWeil.mulByInt W.toAffine m).degree * r ^ 2 -
        HasseWeil.isogTrace (HasseWeil.mulByInt W.toAffine m)
              (HasseWeil.mulByInt W.toAffine (1 - m)) *
            r *
          s +
      s ^ 2

theorem HasseWeil.degree_quadratic_mulByInt_nonneg.{u_2}
  {F : Type u_2} [Field F] [DecidableEq F]
  {W : WeierstrassCurve F}
  [WeierstrassCurve.IsElliptic W.toAffine]
  (m r s : ℤ) (hm : m ≠ 0)
  (hm1 : 1 - m ≠ 0)
  (h_ne : r * m - s ≠ 0) :
  0 ≤
    ↑(HasseWeil.mulByInt W.toAffine
                m).degree *
          r ^ 2 -
        HasseWeil.isogTrace
              (HasseWeil.mulByInt
                W.toAffine m)
              (HasseWeil.mulByInt
                W.toAffine (1 - m)) *
            r *
          s +
      s ^ 2

**Degree quadratic form non-negativity for mulByInt**: for any r, s ∈ ℤ
(with appropriate non-degeneracy), the degree of `[r·m - s]` is
non-negative. This is a direct consequence of degree being a ℕ.

Proof for Theorem 3.3

uses 1

Each value of the form equals a degree (Theorem 3.2), and degrees are cardinalities of function-field extensions, hence \ge 0.

Theorem3.4

uses 1used by 1✓L∃∀N

(Geometric input, packaged.) Suppose the degree form on \operatorname{End}(E) is non-negative on the Frobenius pencil, i.e. for all r, s \in \mathbb{Z} \deg(r\pi - s) \;=\; q\,r^2 - t\,r\,s + s^2 \;\ge\; 0 (Definition 1.5). Then t^2 \le 4q.

Lean code for Theorem3.4●1 theorem

theoremdefined in HasseWeil/Hasse/QuadraticForm.lean

complete

theorem HasseWeil.traceOfFrobenius_sq_le_of_qf_nonneg.{u_1} {K : Type u_1}
  [Field K] [Fintype K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine] (t : ℤ)
  (h_qf_nonneg :
    ∀ (r s : ℤ), 0 ≤ ↑(Fintype.card K) * r ^ 2 - t * r * s + s ^ 2) :
  t ^ 2 ≤ 4 * ↑(Fintype.card K)

theorem HasseWeil.traceOfFrobenius_sq_le_of_qf_nonneg.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  (t : ℤ)
  (h_qf_nonneg :
    ∀ (r s : ℤ),
      0 ≤
        ↑(Fintype.card K) * r ^ 2 -
            t * r * s +
          s ^ 2) :
  t ^ 2 ≤ 4 * ↑(Fintype.card K)

**Discriminant bound, non-negativity form**. Same as
`traceOfFrobenius_sq_le_of_witness` but takes the QF non-negativity hypothesis
directly, with no isogeny family parameter.

Proof for Theorem 3.4

uses 1

The degree of an isogeny is a non-negative integer, and on the rank-two lattice \mathbb{Z}\,1 \oplus \mathbb{Z}\,\pi \subseteq \operatorname{End}(E) it is the binary quadratic form Q(s, r) = s^2 - t\,r\,s + q\,r^2 whose middle coefficient is the Frobenius trace and whose leading coefficient \deg\pi = q. Non-negativity of a binary quadratic form forces its discriminant to be non-positive; here that is exactly t^2 - 4q \le 0. Formally this is the arithmetic core (Theorem 5.1) applied to the degree values.