The Hasse Bound — Lean blueprint

2. The dual isogeny and the trace🔗

Definition2.1
Statement uses 2
Statement dependency previews
Preview
Definition 1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Following Silverman III.6.1, a dual \hat\varphi of an isogeny \varphi is an isogeny in the opposite direction with \hat\varphi \circ \varphi \;=\; [\deg\varphi] \;=\; \varphi \circ \hat\varphi (Definition 1.2, Theorem 1.4). A dual has the same degree as \varphi (Silverman III.6.2(a)). In Hasse-Weil this is the relation IsDualOf, used as the hypothesis language across the degree-form development.

Lean code for Definition2.1●2 declarations
  • defdefined in HasseWeil/DualIsogeny.lean
    complete
    def HasseWeil.IsDualOf.{u_1} {F : Type u_1} [Field F] [DecidableEq F]
  (E : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic E]
  (β α : HasseWeil.Isogeny E E) : Prop
    def HasseWeil.IsDualOf.{u_1} {F : Type u_1}
  [Field F] [DecidableEq F]
  (E : WeierstrassCurve.Affine F)
  [WeierstrassCurve.IsElliptic E]
  (β α : HasseWeil.Isogeny E E) : Prop
    The dual-isogeny relation: `β` is a (left and right) dual of `α`.
  • theoremdefined in HasseWeil/DualIsogeny.lean
    complete
    theorem HasseWeil.degree_dual_of_witness.{u_1} {F : Type u_1} [Field F]
  [DecidableEq F] (E : WeierstrassCurve.Affine F)
  [WeierstrassCurve.IsElliptic E] (α dual : HasseWeil.Isogeny E E)
  (hα : 0 < α.degree) (h_dual : HasseWeil.IsDualOf E dual α) :
  dual.degree = α.degree
    theorem HasseWeil.degree_dual_of_witness.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  (E : WeierstrassCurve.Affine F)
  [WeierstrassCurve.IsElliptic E]
  (α dual : HasseWeil.Isogeny E E)
  (hα : 0 < α.degree)
  (h_dual : HasseWeil.IsDualOf E dual α) :
  dual.degree = α.degree
    Witness-parametric **Silverman III.6.2(a)**: a witness dual of `α` has
degree equal to `α.degree` (for nonzero `α`).
Theorem2.2
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 2.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

(Duality is additive — bilinearity of the degree pairing.) Taking duals is additive on point maps: \widehat{\varphi + \psi} = \hat\varphi + \hat\psi at the level of \operatorname{End}(E) (Silverman III.6.2(c)). This is the algebraic engine making \deg a quadratic form, with the associated pairing \langle\varphi,\psi\rangle = \deg(\varphi+\psi) - \deg\varphi - \deg\psi bilinear (Definition 2.1).

Lean code for Theorem2.2●2 theorems
  • theoremdefined in HasseWeil/DualIsogeny.lean
    complete
    theorem HasseWeil.dual_add_of_trace_witnesses.{u_1} {F : Type u_1} [Field F]
  [DecidableEq F] (E : WeierstrassCurve.Affine F)
  [WeierstrassCurve.IsElliptic E]
  (α β αβ α_dual β_dual αβ_dual : HasseWeil.Isogeny E E) (tα tβ tαβ : ℤ)
  (hαβ_hom : αβ.toAddMonoidHom = α.toAddMonoidHom + β.toAddMonoidHom)
  (hα_trace :
    α.toAddMonoidHom + α_dual.toAddMonoidHom =
      (HasseWeil.mulByInt E tα).toAddMonoidHom)
  (hβ_trace :
    β.toAddMonoidHom + β_dual.toAddMonoidHom =
      (HasseWeil.mulByInt E tβ).toAddMonoidHom)
  (hαβ_trace :
    αβ.toAddMonoidHom + αβ_dual.toAddMonoidHom =
      (HasseWeil.mulByInt E tαβ).toAddMonoidHom)
  (h_tr_add : tαβ = tα + tβ) :
  αβ_dual.toAddMonoidHom = α_dual.toAddMonoidHom + β_dual.toAddMonoidHom
    theorem HasseWeil.dual_add_of_trace_witnesses.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  (E : WeierstrassCurve.Affine F)
  [WeierstrassCurve.IsElliptic E]
  (α β αβ α_dual β_dual αβ_dual :
    HasseWeil.Isogeny E E)
  (tα tβ tαβ : ℤ)
  (hαβ_hom :
    αβ.toAddMonoidHom =
      α.toAddMonoidHom + β.toAddMonoidHom)
  (hα_trace :
    α.toAddMonoidHom +
        α_dual.toAddMonoidHom =
      (HasseWeil.mulByInt E
          tα).toAddMonoidHom)
  (hβ_trace :
    β.toAddMonoidHom +
        β_dual.toAddMonoidHom =
      (HasseWeil.mulByInt E
          tβ).toAddMonoidHom)
  (hαβ_trace :
    αβ.toAddMonoidHom +
        αβ_dual.toAddMonoidHom =
      (HasseWeil.mulByInt E
          tαβ).toAddMonoidHom)
  (h_tr_add : tαβ = tα + tβ) :
  αβ_dual.toAddMonoidHom =
    α_dual.toAddMonoidHom +
      β_dual.toAddMonoidHom
    **Silverman III.6.2(c) — witness-parametric form**.

Given witness duals `α_dual`, `β_dual`, `αβ_dual` for `α`, `β`,
`αβ = α + β`, each satisfying its trace identity at the `AddMonoidHom`
level (with integer traces `tα`, `tβ`, `tαβ`), and integer trace
additivity `tαβ = tα + tβ`, conclude

  `αβ_dual.toAddMonoidHom = α_dual.toAddMonoidHom + β_dual.toAddMonoidHom`.

This is the core mathematical content of III.6.2(c) as a pure algebraic
identity, stated entirely on explicit witnesses (the choice-based
`isogDual` is gone — its underlying `exists_dual` was refuted).
Combines with trace additivity (from III.6.3 QF + III.8) to give
Silverman III.6.2(c) in the witness-parametric style used across
`DegreeQuadraticForm.lean`.
  • theoremdefined in HasseWeil/DualIsogeny.lean
    complete
    theorem HasseWeil.dual_add_of_sum_witnesses.{u_1} {F : Type u_1} [Field F]
  [DecidableEq F] (E : WeierstrassCurve.Affine F)
  [WeierstrassCurve.IsElliptic E]
  (α β αβ α_dual β_dual αβ_dual : HasseWeil.Isogeny E E)
  (hαβ_hom : αβ.toAddMonoidHom = α.toAddMonoidHom + β.toAddMonoidHom)
  (h_sum :
    α.toAddMonoidHom + α_dual.toAddMonoidHom +
        (β.toAddMonoidHom + β_dual.toAddMonoidHom) =
      αβ.toAddMonoidHom + αβ_dual.toAddMonoidHom) :
  αβ_dual.toAddMonoidHom = α_dual.toAddMonoidHom + β_dual.toAddMonoidHom
    theorem HasseWeil.dual_add_of_sum_witnesses.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  (E : WeierstrassCurve.Affine F)
  [WeierstrassCurve.IsElliptic E]
  (α β αβ α_dual β_dual αβ_dual :
    HasseWeil.Isogeny E E)
  (hαβ_hom :
    αβ.toAddMonoidHom =
      α.toAddMonoidHom + β.toAddMonoidHom)
  (h_sum :
    α.toAddMonoidHom +
          α_dual.toAddMonoidHom +
        (β.toAddMonoidHom +
          β_dual.toAddMonoidHom) =
      αβ.toAddMonoidHom +
        αβ_dual.toAddMonoidHom) :
  αβ_dual.toAddMonoidHom =
    α_dual.toAddMonoidHom +
      β_dual.toAddMonoidHom
    **Silverman III.6.2(c) — minimal witness form**: simpler statement of
`dual_add_of_trace_witnesses` taking a single combined sum identity
at the `AddMonoidHom` level, without mentioning integer traces.

Useful when the caller already has the trace-sum witnesses bundled
together pairwise.
Proof for Theorem 2.2
uses 0

The composition \widehat{(\varphi+\psi)} \circ (\varphi+\psi) expands, via the dual-composition and trace-sum witnesses, into [\deg\varphi] + [\deg\psi] + (\text{cross terms}); matching point maps gives additivity of the dual.

Definition2.3
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 2.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The trace of an endomorphism \alpha (with 1-\alpha supplied) is \operatorname{tr}(\alpha) \;=\; 1 + \deg\alpha - \deg(1-\alpha) \;\in\; \mathbb{Z} (Silverman III.8). It is the linear coefficient of the degree quadratic form; for Frobenius, \operatorname{tr}(\pi) = q + 1 - \#E(\mathbb{F}_q) (Definition 1.5).

Lean code for Definition2.3●1 definition
  • defdefined in HasseWeil/Endomorphism.lean
    complete
    def HasseWeil.isogTrace.{u_1} {F : Type u_1} [Field F] [DecidableEq F]
  {E : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic E]
  (α one_sub_α : HasseWeil.Isogeny E E) : ℤ
    def HasseWeil.isogTrace.{u_1} {F : Type u_1}
  [Field F] [DecidableEq F]
  {E : WeierstrassCurve.Affine F}
  [WeierstrassCurve.IsElliptic E]
  (α one_sub_α : HasseWeil.Isogeny E E) :
  ℤ
    The trace of an endomorphism isogeny α, defined by
`tr(α) = 1 + deg(α) - deg(1 - α)`.

The isogeny `1 - α` must be supplied with its degree.
For `α = [n]`, we have `1 - α = [1-n]` with degree `(1-n)²`,
giving `tr([n]) = 1 + n² - (1-n)² = 2n`.

Reference: Silverman III.8, Sutherland Lecture 7.
Theorem2.4
Statement uses 2
Statement dependency previews
Preview
Theorem 1.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 1.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For the scalar endomorphism [n] (with n \ne 0, 1-n \ne 0), \operatorname{tr}([n]) \;=\; 1 + n^2 - (1-n)^2 \;=\; 2n (Definition 2.3, Theorem 1.4).

Lean code for Theorem2.4●1 theorem
  • theoremdefined in HasseWeil/Endomorphism.lean
    complete
    theorem HasseWeil.isogTrace_mulByInt.{u_1} {F : Type u_1} [Field F]
  [DecidableEq F] {E : WeierstrassCurve.Affine F}
  [WeierstrassCurve.IsElliptic E] (n : ℤ) (hn : n ≠ 0)
  (hn1 : 1 - n ≠ 0) :
  HasseWeil.isogTrace (HasseWeil.mulByInt E n)
      (HasseWeil.mulByInt E (1 - n)) =
    2 * n
    theorem HasseWeil.isogTrace_mulByInt.{u_1}
  {F : Type u_1} [Field F] [DecidableEq F]
  {E : WeierstrassCurve.Affine F}
  [WeierstrassCurve.IsElliptic E] (n : ℤ)
  (hn : n ≠ 0) (hn1 : 1 - n ≠ 0) :
  HasseWeil.isogTrace
      (HasseWeil.mulByInt E n)
      (HasseWeil.mulByInt E (1 - n)) =
    2 * n
    The trace of `[n]` is `2n` (for `n ≠ 0` and `1-n ≠ 0`).
Proof for Theorem 2.4
uses 0

Substitute \deg[n] = n^2 and \deg[1-n] = (1-n)^2 into the definition of the trace and expand.

Theorem2.5
uses 0used by 1✓L∃∀N

(Frobenius + Verschiebung is its trace.) With V the Verschiebung (the dual of \pi), \pi + V \;=\; [\operatorname{tr}\pi] \quad\text{and}\quad V(\pi(P)) = q\,P, the diagonal value of the degree pairing on (1,-\pi) (Silverman III.6.2(b)). This is the substantive identity feeding the polarisation degree formula.

Lean code for Theorem2.5●2 theorems
  • theoremdefined in HasseWeil/Hasse/SumTrace.lean
    complete
    theorem HasseWeil.sum_trace_frobenius_witness.{u_1} {K : Type u_1} [Field K]
  [Fintype K] [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine] (hq : 2 ≤ Fintype.card K)
  (h_subset :
    (HasseWeil.mulByInt W.toAffine ↑(Fintype.card K)).pullback.range ≤
      (HasseWeil.frobeniusIsog W).pullback.range)
  (one_sub_V : HasseWeil.Isogeny W.toAffine W.toAffine)
  (h_one_sub_V_hom :
    one_sub_V.toAddMonoidHom =
      AddMonoidHom.id W.toAffine.Point -
        (HasseWeil.verschiebungIsog_of_witness W
            h_subset).toAddMonoidHom)
  (h_one_sub_isDual :
    HasseWeil.IsDualOf W.toAffine one_sub_V
      (HasseWeil.isogOneSub_negFrobenius W hq)) :
  (HasseWeil.frobeniusIsog W).toAddMonoidHom +
      (HasseWeil.verschiebungIsog_of_witness W
          h_subset).toAddMonoidHom =
    (HasseWeil.mulByInt W.toAffine
        (HasseWeil.isogTrace (HasseWeil.frobeniusIsog W)
          (HasseWeil.isogOneSub_negFrobenius W hq))).toAddMonoidHom
    theorem HasseWeil.sum_trace_frobenius_witness.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  (hq : 2 ≤ Fintype.card K)
  (h_subset :
    (HasseWeil.mulByInt W.toAffine
            ↑(Fintype.card
                K)).pullback.range ≤
      (HasseWeil.frobeniusIsog
            W).pullback.range)
  (one_sub_V :
    HasseWeil.Isogeny W.toAffine
      W.toAffine)
  (h_one_sub_V_hom :
    one_sub_V.toAddMonoidHom =
      AddMonoidHom.id W.toAffine.Point -
        (HasseWeil.verschiebungIsog_of_witness
            W h_subset).toAddMonoidHom)
  (h_one_sub_isDual :
    HasseWeil.IsDualOf W.toAffine
      one_sub_V
      (HasseWeil.isogOneSub_negFrobenius W
        hq)) :
  (HasseWeil.frobeniusIsog
          W).toAddMonoidHom +
      (HasseWeil.verschiebungIsog_of_witness
          W h_subset).toAddMonoidHom =
    (HasseWeil.mulByInt W.toAffine
        (HasseWeil.isogTrace
          (HasseWeil.frobeniusIsog W)
          (HasseWeil.isogOneSub_negFrobenius
            W hq))).toAddMonoidHom
    **Sum-trace identity for Frobenius + Verschiebung** (Silverman
III.6.2(b), Hasse case): given the Session-3 inclusion `Im([q]*) ⊆ Im(π*)`
(which makes `verschiebungIsog_of_witness` a genuine isogeny dual to
Frobenius), an auxiliary `1 − V` isogeny with the standard hom-form, and
the substantive III.6.2(b) ingredient `IsDualOf (1 − V) (1 − π)`,
conclude

  `π + V = [tr π]`

at the `toAddMonoidHom` level, where `tr π = isogTrace π (1 − π) =
1 + q − deg(1 − π)`. Worker D consumes this as `h_sum_trace` for the
`degree_quadratic_genuine_addIsog` instance with `α = π`.

The Frobenius half of the dual chain comes from
`verschiebungIsog_of_witness_isDualOf_frobenius` (Worker C, Session 5).
The `(1 − π) ∘ (1 − V) = [deg(1 − π)]` ingredient is the substantive
III.6.2(b) input — it's the one piece that doesn't reduce to the existing
chain and needs to be supplied separately (or proved from universal
dual-additivity in a future closure).
  • theoremdefined in HasseWeil/Hasse/SumTrace.lean
    complete
    theorem HasseWeil.dual_comp_frobenius_witness.{u_1} {K : Type u_1} [Field K]
  [Fintype K] [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  (h_subset :
    (HasseWeil.mulByInt W.toAffine ↑(Fintype.card K)).pullback.range ≤
      (HasseWeil.frobeniusIsog W).pullback.range)
  (P : W.toAffine.Point) :
  (HasseWeil.verschiebungIsog_of_witness W h_subset).toAddMonoidHom
      ((HasseWeil.frobeniusIsog W).toAddMonoidHom P) =
    ↑(HasseWeil.frobeniusIsog W).degree • P
    theorem HasseWeil.dual_comp_frobenius_witness.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  (h_subset :
    (HasseWeil.mulByInt W.toAffine
            ↑(Fintype.card
                K)).pullback.range ≤
      (HasseWeil.frobeniusIsog
            W).pullback.range)
  (P : W.toAffine.Point) :
  (HasseWeil.verschiebungIsog_of_witness W
          h_subset).toAddMonoidHom
      ((HasseWeil.frobeniusIsog
            W).toAddMonoidHom
        P) =
    ↑(HasseWeil.frobeniusIsog W).degree •
      P
    **Dual-composition for Frobenius + Verschiebung** (`h_dual_comp` form):
`V(π(P)) = q • P` for every `P : E.Point`. Discharges Worker D's
`h_dual_comp` hypothesis in `degree_quadratic_genuine_addIsog` for the
`α = π` instance. Direct from `verschiebungIsog_of_witness_isDualOf_frobenius`'s
first conjunct + `frobeniusIsog_degree`.
Proof for Theorem 2.5
Proof uses 3
Proof dependency previews
Preview
Definition 1.6
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

V \circ \pi = [\deg\pi] = [q] from the dual relation (Definition 2.1, Definition 1.6); the sum-trace identity is then the (1-\pi)\circ(1-V) = [\deg(1-\pi)] bilinear-form value rearranged via additivity of the dual (Theorem 2.2).