The naïve height and the approximate parallelogram law

This file defines the naïve height on an elliptic curve (over a field F with a theory of heights, i.e., satisfying [Height.AdmissibleAbsValues F]).

We then prove the approximate parallelogram law for (affine) points on elliptic curves,

  |h(P+Q) + h(P-Q) - 2*(h(P) + h(Q))| ≤ C

where h is the naïve height, P and Q are affine points on a WeierstrassCurve and C is some real constant depending only on the Weierstrass model.

noncomputable def WeierstrassCurve.Affine.Point.naiveHeight {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] {W : Affine F} (P : W.Point) : ℝ

The naïve logarithmic height of an affine point on W.

Equations

• P.naiveHeight = Height.logHeight P.xRep

theorem WeierstrassCurve.Affine.Point.naiveHeight_eq_logHeight {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] {W : Affine F} (P : W.Point) : P.naiveHeight = Height.logHeight P.xRep

theorem WeierstrassCurve.Affine.Point.naiveHeight_eq_logHeight₁ {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] {W : Affine F} {P : W.Point} : P.naiveHeight = Height.logHeight₁ (P.xRep 0)

theorem WeierstrassCurve.Affine.abs_logHeight_sym2x_sub_le {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] (W : Affine F) : ∃ (C : ℝ), ∀ (P Q : W.Point), |Height.logHeight (P.sym2x Q) - (P.naiveHeight + Q.naiveHeight)| ≤ C

theorem WeierstrassCurve.Affine.abs_logHeight_addSubMap_sub_two_mul_logHeight_le {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : ∃ (C : ℝ), ∀ (x : Fin 3 → F), |(Height.logHeight fun (i : Fin 3) => (MvPolynomial.eval x) (addSubMap W i)) - 2 * Height.logHeight x| ≤ C

If W is a Weierstrass curve over F, then the map Φ : ℙ² → ℙ² given by addSubMap W is a morphism.

This implies that |logHeight (Φ x) - 2 * logHeight x| ≤ C for a constant C, where x = ![s, t, u] and Φ acts on the coordinate vector.

theorem WeierstrassCurve.Affine.approx_parallelogram_law {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] (W : Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq F] : ∃ (C : ℝ), ∀ (P Q : W.Point), |(P + Q).naiveHeight + (P - Q).naiveHeight - 2 * (P.naiveHeight + Q.naiveHeight)| ≤ C

The approximate parallelogram law for the naïve height on an elliptic curve.

instance WeierstrassCurve.Affine.instNorthcottPointRealNaiveHeightOfLogHeight₁ {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] {W : Affine F} [Northcott Height.logHeight₁] : Northcott Point.naiveHeight

theorem WeierstrassCurve.Affine.finite_naiveHeight_le {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] (W : Affine F) [Northcott Height.logHeight₁] (B : ℝ) : {P : W.Point | P.naiveHeight ≤ B}.Finite

The set of F-points on W with naïve height bounded by B is finite. This is an important ingredient for the Mordell-Weil Theorem.

theorem WeierstrassCurve.Affine.finite_torsion {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] {W : Affine F} [Northcott Height.logHeight₁] [DecidableEq F] [WeierstrassCurve.IsElliptic W] : Finite ↥(AddCommGroup.torsion W.Point)

The group of F-rational torsion points on an elliptic curve is finite when F is a field that has the Northcott property (e.g., a number field).

@[deprecated WeierstrassCurve.Affine.abs_logHeight_addSubMap_sub_two_mul_logHeight_le (since := "2026-09-05")]

theorem WeierstrassCurve.abs_logHeight_addSubMap_sub_two_mul_logHeight_le {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : ∃ (C : ℝ), ∀ (x : Fin 3 → F), |(Height.logHeight fun (i : Fin 3) => (MvPolynomial.eval x) (addSubMap W i)) - 2 * Height.logHeight x| ≤ C

Alias of WeierstrassCurve.Affine.abs_logHeight_addSubMap_sub_two_mul_logHeight_le.

---

If W is a Weierstrass curve over F, then the map Φ : ℙ² → ℙ² given by addSubMap W is a morphism.

This implies that |logHeight (Φ x) - 2 * logHeight x| ≤ C for a constant C, where x = ![s, t, u] and Φ acts on the coordinate vector.