The explicit descent boundary for X₁(11) #
For the rational elliptic curve
v² + v = u³ - u²,
this file separates the routine Mordell--Weil consequences of a five-descent from its one genuinely arithmetic input. In particular:
- finite index of multiplication by five implies finite generation, by an explicit five-fold version of naïve-height descent;
- the visible point
(0,0)has exact order five; - reduction at three controls rational five-torsion;
- a five-coset certificate for
E(ℚ) / 5 E(ℚ)implies rank zero and finiteness.
The remaining unconditional input is therefore an explicit five-isogeny Selmer calculation producing the five-coset certificate.
The approximate parallelogram law is strong enough to run descent with multiplication by five.
Multiplication by five on the rational point group.
Equations
Instances For
The visible point (0,0) has exact additive order five.
The Vélu quotient of curve by the visible order-five subgroup.
It is the minimal curve customarily labelled 11a1.
Equations
- MazurTorsion.XOneEleven.fiveIsogenousCurve = { a₁ := 0, a₂ := -1, a₃ := 1, a₄ := -10, a₆ := -20 }
Instances For
The explicit Vélu formulas carry the affine equation for curve
to the affine equation for its five-isogenous quotient whenever the
input is outside the kernel.
The factorization used in the proof is
F'(φ(x,y)) = -(x³-4x²+4x-2)² (x³-x²-y²-y) (x³+x²+x-1)² / (x⁶(x-1)⁶).
The denominator-safe affine part of the explicit Vélu map.
Equations
Instances For
The denominator-safe candidate Vélu map, sending the point at
infinity and the four points with abscissa 0 or 1 to infinity.
Its coordinate identity and zero fiber are checked here. Proving that it preserves addition is a separate (substantial) rational-function calculation and is not smuggled into the definition.
Equations
- MazurTorsion.XOneEleven.veluFiveMap WeierstrassCurve.Affine.Point.zero = 0
- MazurTorsion.XOneEleven.veluFiveMap (WeierstrassCurve.Affine.Point.some x_1 y hP) = if hx : x_1 = 0 ∨ x_1 = 1 then 0 else MazurTorsion.XOneEleven.veluFivePoint hP ⋯ ⋯
Instances For
The affine zero fiber of the candidate Vélu map is exactly the
four nonzero points with abscissa 0 or 1.
Miller's degree-five function attached to the kernel generator.
On the smooth projective curve its divisor is
5(P00) - 5(O); the displayed formula is the input for the Kummer
map in a five-isogeny descent.
Instances For
The subgroup of rational points killed by five.
Equations
Instances For
Restriction of reduction modulo three to rational five-torsion.
Equations
Instances For
Good reduction at three is injective on rational five-torsion.
There are at most five rational points killed by five.
The five multiples of (0,0), regarded as points killed by five.
Equations
Instances For
The rational five-torsion subgroup consists of exactly the five
multiples of (0,0).
Every rational point killed by five is one of the five multiples
of (0,0).
The five proposed representatives for
E(ℚ) / 5 E(ℚ).
Instances For
The exact arithmetic output required from a five-isogeny descent: every rational point differs from one of the five visible torsion points by a multiple of five.
This is deliberately a proposition rather than a class or a hidden assumption. A future Selmer computation can prove it and feed the theorem below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A five-coset bound gives a surjection onto the quotient by multiplication by five.
A five-coset bound makes multiplication by five have finite index.
A five-coset bound implies finite generation by the explicit five-fold height descent above.
A five-coset bound gives the sharp index estimate
[E(ℚ) : 5 E(ℚ)] ≤ 5.
The five-coset output of a five-isogeny descent forces Mordell--Weil rank zero.
Once the five explicit cosets have been certified, every rational point is torsion and the rational point group is finite.
End-to-end consequence of the isolated five-descent boundary: the rational point group has exactly five elements, and every affine point has abscissa zero or one.