Documentation

MazurTorsion.NumberTheory.XOneEighteenDescent

Quotient and arithmetic descent identities for X₁(18) #

The order-three automorphism of the order-eighteen sextic has invariant functions

u = (x³ - 3x + 1)/(x(x-1)), v = y/(x(x-1)),

which satisfy

v² = u² - 4u + 12.

This file parameterizes that rational conic, identifies the degree-three fiber as the cyclic cubic

z³ - uz² + (u-3)z + 1,

and records its orbit factorization and square discriminant. After the conic parameter is introduced, the cleared cubic has discriminant

(t²+3)²(7t²+6t+3)².

The two quadratic factors are explicit norms in Eisenstein coordinates. Writing ω²+ω+1=0, the second is

N((3+ω)m + (1-ω)n) = 7m²+6mn+3n²,

and N(3+ω)=7. We prove these norm identities, multiplicativity, two primitive-form Bézout identities, and the fact that the two norm forms cannot both be divisible by 7 for coprime integer parameters.

For a rational root, comparison of all three coefficients of the cyclic cubic gives two binary quadratic--cubic identities. Their resultant is 16; a mod-2 and mod-16 calculation then proves that the remaining integer quotient is one of -8, -4, 4, or 8. The final boundary is therefore a four-case primitive integral obstruction.

These are algebraic and local prerequisites for the classical π = 3+ω descent. They do not construct the induced endomorphism of the Jacobian, prove π-surjectivity on its Mordell--Weil group, determine its torsion, or solve the four remaining integral cases.

The rational conic quotient #

The conic abscissa obtained from a line through (u,v)=(1,3).

Equations
Instances For

    The conic ordinate obtained from the same line.

    Equations
    Instances For

      The displayed parametrization lies on the invariant conic.

      The slope used to recover the conic parameter away from u=1.

      Equations
      Instances For
        theorem MazurTorsion.XOneEighteenDescent.conic_parameter_inverse (u v : ℚ) (hu : u ≠ 1) (hconic : v ^ 2 = u ^ 2 - 4 * u + 12) :
        have t := conicSlope u v; t ^ 2 ≠ 1 ∧ conicU t = u ∧ conicV t = v

        Away from the base point's vertical fiber, the slope construction recovers both conic coordinates.

        theorem MazurTorsion.XOneEighteenDescent.conic_at_one_iff (v : ℚ) :
        v ^ 2 = 1 ^ 2 - 4 * 1 + 12 ↔ v = 3 ∨ v = -3

        The exceptional affine conic fiber u=1 consists of v=±3.

        theorem MazurTorsion.XOneEighteenDescent.conic_rational_parameterization (u v : ℚ) (hconic : v ^ 2 = u ^ 2 - 4 * u + 12) :
        u = 1 ∧ (v = 3 ∨ v = -3) ∨ ∃ (t : ℚ), t ^ 2 ≠ 1 ∧ conicU t = u ∧ conicV t = v

        Every rational affine point on the invariant conic is either one of the two exceptional points over u=1, or comes from the displayed one-parameter family.

        The cyclic cubic fiber #

        The degree-three fiber above a quotient abscissa u.

        Equations
        Instances For

          The exceptional quotient fiber u=1 has no rational abscissa.

          The invariant abscissa of a noncuspidal point satisfies its cubic fiber equation.

          A noncuspidal rational abscissa never lies over the exceptional quotient value u=1.

          Product over the three-element Möbius orbit, viewed as a degree-three norm polynomial.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The orbit norm is exactly the cyclic cubic fiber polynomial.

            The standard discriminant formula for a cubic a z³ + b z² + c z + d.

            Equations
            Instances For

              The cyclic cubic fiber has square discriminant.

              The conic-parameterized cubic with its sole denominator cleared.

              Equations
              Instances For

                Clearing the conic denominator gives clearedFiber.

                theorem MazurTorsion.XOneEighteenDescent.clearedFiber_eq_zero (t z : ℚ) (ht : t ^ 2 ≠ 1) (hroot : fiberCubic (conicU t) z = 0) :

                A root of the parameterized fiber gives a root of the cleared cubic.

                The homogeneous cubic obtained by writing the conic parameter as t=m/n.

                Equations
                Instances For

                  Substitution t=m/n turns the cleared cubic into its homogeneous form after multiplication by n².

                  A root of the cleared rational-parameter cubic is a root of the primitive homogeneous cubic attached to its canonical fraction.

                  theorem MazurTorsion.XOneEighteenDescent.homogeneousFiber_discriminant (m n : ℚ) :
                  cubicDiscriminant (m ^ 2 - n ^ 2) (-(m ^ 2 - 6 * m * n - 3 * n ^ 2)) (-2 * m ^ 2 - 6 * m * n) (m ^ 2 - n ^ 2) = (m ^ 2 + 3 * n ^ 2) ^ 2 * (7 * m ^ 2 + 6 * m * n + 3 * n ^ 2) ^ 2

                  The homogeneous cubic discriminant is the product of the squares of the two quadratic norm forms.

                  Every rational noncuspidal point on the sextic admits the explicit conic parameter and is a root of the resulting denominator-free cubic.

                  Canonical numerator-denominator coordinates sharpen the preceding statement to primitive integer parameters.

                  theorem MazurTorsion.XOneEighteenDescent.clearedFiber_discriminant (t : ℚ) :
                  cubicDiscriminant (t ^ 2 - 1) (-(t ^ 2 - 6 * t - 3)) (-2 * t ^ 2 - 6 * t) (t ^ 2 - 1) = (t ^ 2 + 3) ^ 2 * (7 * t ^ 2 + 6 * t + 3) ^ 2

                  The coefficient discriminant of the cleared cubic factors into two squared quadratic forms.

                  theorem MazurTorsion.XOneEighteenDescent.fiber_discriminant_parameter_factorization (t : ℚ) (ht : t ^ 2 ≠ 1) :
                  conicU t ^ 2 - 3 * conicU t + 9 = (t ^ 2 + 3) * (7 * t ^ 2 + 6 * t + 3) / (t ^ 2 - 1) ^ 2

                  The square root of the fiber discriminant before clearing denominators factors as displayed.

                  Eisenstein-coordinate norm identities #

                  Multiplication in coordinates a+bω, where ω²+ω+1=0.

                  Equations
                  Instances For

                    The norm of the Eisenstein coordinate pair a+bω.

                    Equations
                    Instances For

                      Complex conjugation in coordinates a+bω, using conj(ω)=ω²=-1-ω.

                      Equations
                      Instances For

                        Multiplication by the conjugate gives the rational integer norm.

                        The Eisenstein prime above 7, represented by π=3+ω.

                        Equations
                        Instances For

                          The coordinate factorization of the rational prime 7 as π·conj(π).

                          The index-seven lattice cut out by multiplication by π has the single congruence 2a+b ≡ 0 mod 7.

                          A factor of π forces a factor of 7 in the norm.

                          The first quadratic factor is an Eisenstein norm after clearing a rational parameter t=m/n.

                          The second quadratic factor is the norm of πm + (1-ω)n.

                          Coordinate identity behind (3+ω)m + (1-ω)n = (3m+n) + (m-n)ω.

                          theorem MazurTorsion.XOneEighteenDescent.eisenstein_cube_coordinates (a b : ℤ) :
                          eisensteinMul (eisensteinMul (a, b) (a, b)) (a, b) = (a ^ 3 - 3 * a * b ^ 2 + b ^ 3, 3 * (a * b * (a - b)))

                          The cube of a+bω in integral Eisenstein coordinates.

                          theorem MazurTorsion.XOneEighteenDescent.parameter_eisenstein_product (m n : ℤ) :
                          eisensteinMul (0, 1) (eisensteinMul (m + n, 2 * n) (eisensteinConj (3 * m + n, m - n))) = (m ^ 2 - 6 * m * n - 3 * n ^ 2, 3 * (m ^ 2 - n ^ 2))

                          Up to multiplication by ω, the two norm arguments multiply to the pair formed by the trace coefficient and three times the leading coefficient of the split cubic.

                          theorem MazurTorsion.XOneEighteenDescent.split_parameter_eisenstein_product_eq_scalar_cube (m n a b k : ℤ) (hk : m ^ 2 - n ^ 2 = k * (a * b * (a - b))) (htrace : m ^ 2 - 6 * m * n - 3 * n ^ 2 = k * (a ^ 3 - 3 * a * b ^ 2 + b ^ 3)) :

                          The two split-coefficient identities package as a scalar-times-cube factorization in integral Eisenstein coordinates. This is the direct input for the remaining unique-factorization argument.

                          The second norm argument is divisible by π exactly when the denominator parameter is divisible by 7.

                          The two primitive quadratic norm forms.

                          Equations
                          Instances For

                            The norm form associated to the Eisenstein prime above seven.

                            Equations
                            Instances For
                              theorem MazurTorsion.XOneEighteenDescent.homogeneousFiber_discriminant_integer (m n : ℤ) :
                              cubicDiscriminant (↑m ^ 2 - ↑n ^ 2) (-(↑m ^ 2 - 6 * ↑m * ↑n - 3 * ↑n ^ 2)) (-2 * ↑m ^ 2 - 6 * ↑m * ↑n) (↑m ^ 2 - ↑n ^ 2) = ↑(firstParameterForm m n) ^ 2 * ↑(piParameterForm m n) ^ 2

                              For integer homogeneous parameters, the two factors in the cubic discriminant are exactly the two named norm forms.

                              A Bézout-style identity eliminating the denominator parameter.

                              A complementary Bézout-style identity eliminating the numerator parameter.

                              For primitive integer parameters, the two Eisenstein norm forms cannot both be divisible by the rational prime below π.

                              Rational-root divisibility #

                              theorem MazurTorsion.XOneEighteenDescent.root_orbit_product_dvd_leadingCoefficient (m n a b : ℤ) (hab : IsCoprime a b) (hroot : homogeneousFiber (↑m) (↑n) (↑a / ↑b) = 0) (hb : b ≠ 0) :
                              a * b * (a - b) ∣ m ^ 2 - n ^ 2

                              If a primitive rational number a/b is a root of the homogeneous cyclic cubic, then the three pairwise-coprime cusp factors of its Möbius orbit divide the leading coefficient together.

                              theorem MazurTorsion.XOneEighteenDescent.parameter_forms_mul_orbitNorm_sq (m n a b : ℤ) (hn : n ≠ 0) (hb : b ≠ 0) (ha : a ≠ 0) (hab : a ≠ b) (ht : (↑m / ↑n) ^ 2 ≠ 1) (hU : conicU (↑m / ↑n) = XOneEighteenFiniteField.invariantX (↑a / ↑b)) :
                              firstParameterForm m n * piParameterForm m n * (a * b * (a - b)) ^ 2 = (m ^ 2 - n ^ 2) ^ 2 * (a ^ 2 - a * b + b ^ 2) ^ 3

                              Equating the two presentations of the cyclic-cubic discriminant gives an integral norm equation for primitive quotient and root coordinates.

                              theorem MazurTorsion.XOneEighteenDescent.exists_root_leadingCoefficient_quotient (m n a b : ℤ) (hn : n ≠ 0) (hb : b ≠ 0) (ha : a ≠ 0) (hab : a ≠ b) (ht : (↑m / ↑n) ^ 2 ≠ 1) (hU : conicU (↑m / ↑n) = XOneEighteenFiniteField.invariantX (↑a / ↑b)) (hdvd : a * b * (a - b) ∣ m ^ 2 - n ^ 2) :
                              ∃ (k : ℤ), m ^ 2 - n ^ 2 = k * (a * b * (a - b)) ∧ firstParameterForm m n * piParameterForm m n = k ^ 2 * (a ^ 2 - a * b + b ^ 2) ^ 3

                              After dividing by the nonzero product of the three cusp factors, the discriminant identity becomes a square times the cube of the Eisenstein orbit norm.

                              theorem MazurTorsion.XOneEighteenDescent.root_split_coefficient_identities (m n a b k : ℤ) (hn : n ≠ 0) (hb : b ≠ 0) (ha : a ≠ 0) (hab : a ≠ b) (ht : (↑m / ↑n) ^ 2 ≠ 1) (hU : conicU (↑m / ↑n) = XOneEighteenFiniteField.invariantX (↑a / ↑b)) (hk : m ^ 2 - n ^ 2 = k * (a * b * (a - b))) :
                              m ^ 2 - 6 * m * n - 3 * n ^ 2 = k * (a ^ 3 - 3 * a * b ^ 2 + b ^ 3) ∧ -2 * m ^ 2 - 6 * m * n = k * (a ^ 3 - 3 * a ^ 2 * b + b ^ 3)

                              Once the quotient parameter and a primitive rational root are both cleared, equality of the two invariant presentations determines the other two coefficients of the split cyclic cubic.

                              theorem MazurTorsion.XOneEighteenDescent.split_parameters_odd (m n a b k : ℤ) (hmn : IsCoprime m n) (hab : IsCoprime a b) (hk : m ^ 2 - n ^ 2 = k * (a * b * (a - b))) (htrace : m ^ 2 - 6 * m * n - 3 * n ^ 2 = k * (a ^ 3 - 3 * a * b ^ 2 + b ^ 3)) (hpair : -2 * m ^ 2 - 6 * m * n = k * (a ^ 3 - 3 * a ^ 2 * b + b ^ 3)) :
                              Odd m ∧ Odd n

                              A primitive split fiber can only occur in the odd-odd parameter class. Opposite parity would give the rootless cubic z³ + z² + 1 modulo two.

                              theorem MazurTorsion.XOneEighteenDescent.split_parameter_resultant_identities (m n : ℤ) :
                              (15 * m + 9 * n) * (m ^ 2 - n ^ 2) + (m - 3 * n) * (m ^ 2 - 6 * m * n - 3 * n ^ 2) = 16 * m ^ 3 ∧ (3 * m - 19 * n) * (m ^ 2 - n ^ 2) + (-3 * m + n) * (m ^ 2 - 6 * m * n - 3 * n ^ 2) = 16 * n ^ 3

                              The two independent split-fiber coefficients have resultant sixteen as binary quadratic forms in the primitive conic parameters.

                              theorem MazurTorsion.XOneEighteenDescent.split_quotient_divisibility (m n a b k : ℤ) (hmn : IsCoprime m n) (hab : IsCoprime a b) (hk : m ^ 2 - n ^ 2 = k * (a * b * (a - b))) (htrace : m ^ 2 - 6 * m * n - 3 * n ^ 2 = k * (a ^ 3 - 3 * a * b ^ 2 + b ^ 3)) (hpair : -2 * m ^ 2 - 6 * m * n = k * (a ^ 3 - 3 * a ^ 2 * b + b ^ 3)) :
                              Odd m ∧ Odd n ∧ 4 ∣ k ∧ ¬16 ∣ k ∧ k ∣ 16

                              Primitivity and the split coefficient identities make the apparent quotient k a divisor of sixteen with exact two-adic order two or three. In particular, the remaining arithmetic boundary has only four possible signed values for k.

                              theorem MazurTorsion.XOneEighteenDescent.split_quotient_eq_neg_eight_or_neg_four_or_four_or_eight (m n a b k : ℤ) (hmn : IsCoprime m n) (hab : IsCoprime a b) (hk : m ^ 2 - n ^ 2 = k * (a * b * (a - b))) (htrace : m ^ 2 - 6 * m * n - 3 * n ^ 2 = k * (a ^ 3 - 3 * a * b ^ 2 + b ^ 3)) (hpair : -2 * m ^ 2 - 6 * m * n = k * (a ^ 3 - 3 * a ^ 2 * b + b ^ 3)) :
                              k = -8 ∨ k = -4 ∨ k = 4 ∨ k = 8

                              The quotient in a primitive split cyclic cubic is one of the four signed integers of two-adic order two or three.

                              theorem MazurTorsion.XOneEighteenDescent.split_quotient_mod_four_cases (m n a b k : ℤ) (hab : IsCoprime a b) (hm : Odd m) (hn : Odd n) (hnorm : firstParameterForm m n * piParameterForm m n = k ^ 2 * (a ^ 2 - a * b + b ^ 2) ^ 3) (hk : k = -8 ∨ k = -4 ∨ k = 4 ∨ k = 8) :
                              k = -8 ∧ ↑m = ↑n ∨ k = -4 ∧ ↑m ≠ ↑n ∨ k = 4 ∧ ↑m ≠ ↑n ∨ k = 8 ∧ ↑m = ↑n

                              Modulo four, the primitive norm identity separates the four possible quotients into two pairs: the parameters agree for quotient ±8 and differ for quotient ±4.

                              theorem MazurTorsion.XOneEighteenDescent.noncuspidal_curve_primitive_descent_data (x y : ℚ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) (hcurve : y ^ 2 = Kubert.orderEighteenHyperellipticPolynomial x) :
                              ∃ (m : ℤ) (n : ℤ) (a : ℤ) (b : ℤ) (k : ℤ), 0 < n ∧ 0 < b ∧ IsCoprime m n ∧ IsCoprime a b ∧ ↑a / ↑b = x ∧ a ≠ 0 ∧ a ≠ b ∧ (↑m / ↑n) ^ 2 ≠ 1 ∧ conicU (↑m / ↑n) = XOneEighteenFiniteField.invariantX (↑a / ↑b) ∧ conicV (↑m / ↑n) = XOneEighteenFiniteField.invariantY x y ∧ homogeneousFiber (↑m) (↑n) (↑a / ↑b) = 0 ∧ m ^ 2 - n ^ 2 = k * (a * b * (a - b)) ∧ firstParameterForm m n * piParameterForm m n = k ^ 2 * (a ^ 2 - a * b + b ^ 2) ^ 3 ∧ ¬(7 ∣ firstParameterForm m n ∧ 7 ∣ piParameterForm m n)

                              The complete elementary descent package obtained here from a noncuspidal rational point. Besides primitive quotient and root coordinates, it supplies the exact quotient of the cubic's leading coefficient by the three cusp factors and the resulting square-times-cube Eisenstein norm equation.

                              The remaining arithmetic statement after the checked quotient and rational-root descent. It rules out primitive integral parameters for which the cyclic cubic has a rational root and satisfies the resulting square-times-cube norm equation.

                              This predicate is deliberately narrower than the original rational-point classification: all coordinate changes, denominator conditions, and norm identities needed to reach it are proved above.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                The finite integral boundary left after comparing all three coefficients of the split cyclic cubic. The quotient is restricted to -8, -4, 4, or 8; no rational functions or denominator conditions remain in the statement.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  The refined finite boundary also exposes the scalar-times-cube Eisenstein product and the modulo-four distinction between quotient ±4 and quotient ±8.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    The refined finite boundary implies the original four-case boundary. Both extra certificates are derived from the old hypotheses, so existing consumers retain their public types.

                                    The finite split-coefficient boundary implies the earlier primitive rational-root obstruction.

                                    The refined finite split boundary implies the primitive rational-root obstruction through the compatibility-preserving four-case interface.

                                    The primitive cyclic-cubic obstruction consumes the complete descent package and rules out a noncuspidal rational point on the X₁(18) model.

                                    A proof of the explicit primitive cyclic-cubic obstruction excludes exact rational order eighteen through the already checked Tate-normal-form and genus-two reduction.

                                    The four-case integral split obstruction excludes exact rational order eighteen through the checked primitive descent.

                                    The scalar-cube and modulo-four refined finite boundary excludes exact rational order eighteen through the compatibility-preserving conversion.