Regulator.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 0 contain sorry, 0 declared as axioms

Heights and the regulator of an elliptic curve

Let K be a field with admissible absolute values. The canonical height is a quadratic form, defined as the limit of 4⁻ⁿhₓ(2ⁿP) as n → ∞. Here, hₓ(P) is the naïve height, which is the logarithm of the maximum of the absolute numerator and denominator of the x-coordinate. The Néron--Tate pairing is the bilinear pairing associated to the canonical height. The regulator is the absolute determinant of the Gram matrix of the Néron--Tate pairing on E(K) modulo torsion.

These definitions are adapted from the Apache-2.0-licensed Tau Ceti files MordellWeil/NaiveHeight.lean, CanonicalHeight.lean, MordellWeil/PointModTorsion.lean, and MordellWeil/Regulator.lean. Over ℚ, the canonical height here is twice Tau Ceti's height, so a rank-r regulator is 2ʳ times Tau Ceti's regulator.

References

[Silverman2009] Joseph H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Graduate Texts in Mathematics 106, Springer (2009), doi. Chapter VIII, §§5–6 and §9: heights, the canonical pairing, and the elliptic regulator; see especially pp. 252–253 and Remark VIII.9.8 for the relative normalization.
Tau Ceti regulator
LMFDB canonical height
LMFDB regulator
[SageMath heights and regulators over number fields]sage-regulator

Imports (7)

Imported by 1 file

FormalConjecturesForMathlib.lean

def WeierstrassCurve.Affine.Point.naiveHeight The logarithmic height hₓ of the x-coordinate with value zero at infinity line 62 source
Source documentation
The logarithmic height hₓ of the x-coordinate with value zero at infinity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Height.AdmissibleAbsValues, WeierstrassCurve.Affine, WeierstrassCurve.Affine.Point, Real
Proof uses: WeierstrassCurve.Affine.Point.naiveHeight.match_1, Unit, OfNat.ofNat, WeierstrassCurve.Affine.Nonsingular, Height.logHeight₁
4 instances, coercions and auxiliary constants left out.
```
def naiveHeight : W.Point → ℝ
  | .zero => 0
  | .some x .. => Height.logHeight₁ x

/-- The canonical height `lim_n 4⁻ⁿhₓ(2ⁿP)` in terms of the logarithmic height `hₓ`. -/
```
def WeierstrassCurve.Affine.Point.canonicalHeight The canonical height lim_n 4⁻ⁿhₓ(2ⁿP) in terms of the logarithmic height hₓ line 67 source
Source documentation
The canonical height lim_n 4⁻ⁿhₓ(2ⁿP) in terms of the logarithmic height hₓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Field, Height.AdmissibleAbsValues, WeierstrassCurve.Affine, WeierstrassCurve.Affine.Point, Real
Proof uses: Filter.limUnder, Nat, Filter.atTop, HDiv.hDiv, WeierstrassCurve.Affine.Point.naiveHeight, HSMul.hSMul, HPow.hPow, OfNat.ofNat
27 instances, coercions and auxiliary constants left out.
```
def canonicalHeight : ℝ := Filter.atTop.limUnder fun n : ℕ ↦ (2 ^ n • P).naiveHeight / 4 ^ n
```
Mentions: WeierstrassCurve.Affine.Point.naiveHeight
def WeierstrassCurve.Affine.Point.neronTatePairing The Néron--Tate height pairing, defined by polarisation of the canonical height line 70 source
Source documentation
The Néron--Tate height pairing, defined by polarisation of the canonical height.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Field, Height.AdmissibleAbsValues, WeierstrassCurve.Affine, WeierstrassCurve.Affine.Point, Real
Proof uses: HDiv.hDiv, HSub.hSub, WeierstrassCurve.Affine.Point.canonicalHeight, HAdd.hAdd, OfNat.ofNat
12 instances, coercions and auxiliary constants left out.
```
def neronTatePairing : ℝ := ((P + Q).canonicalHeight - P.canonicalHeight - Q.canonicalHeight) / 2
```
Mentions: WeierstrassCurve.Affine.Point.canonicalHeight
def WeierstrassCurve.Affine.Point.neronTateMatrix The Gram matrix of the Néron--Tate height pairing on any family of K-rational points line 73 source
Source documentation
The Gram matrix of the Néron--Tate height pairing on any family of K-rational points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Field, Height.AdmissibleAbsValues, WeierstrassCurve.Affine, WeierstrassCurve.Affine.Point, Matrix, Real
Proof uses: Matrix.gram, Inner.mk, WeierstrassCurve.Affine.Point.neronTatePairing
2 instances, coercions and auxiliary constants left out.
```
def neronTateMatrix {ι : Type*} (P : ι → W.Point) : Matrix ι ι ℝ :=
…
```
def WeierstrassCurve.Affine.Point.regulator The absolute determinant of the height pairing on a finite basis of E(K) modulo torsion line 79 source
Source documentation
The absolute determinant of the height pairing on a finite basis of E(K) modulo torsion. For number fields with their standard height instance, this is the non-normalised regulator.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Field, Height.AdmissibleAbsValues, WeierstrassCurve.Affine, Module.Finite, Int, HasQuotient.Quotient, WeierstrassCurve.Affine.Point, Submodule, Submodule.torsion, Real
Proof uses: abs, Matrix.det, Fin, Module.finrank, WeierstrassCurve.Affine.Point.neronTateMatrix, Function.comp, Quotient, Submodule.quotientRel, Quotient.out, Module.Basis, Module.finBasis
33 instances, coercions and auxiliary constants left out.
```
def regulator [Module.Finite ℤ (W.Point ⧸ Submodule.torsion ℤ W.Point)] : ℝ :=
…
```