Documentation

MazurTorsion.NumberTheory.XOneEighteenQuadraticNormBase

Low-level quadratic norm data for the X₁(18) descent #

The anti-diagonal quotient of the surviving cubic correspondence has the genus-two model

z² = 33w⁶ + 18w⁵ + 15w⁴ - 20w³ + 15w² + 2w + 1.

Its sextic admits a useful factorization over ℚ(√-2). In homogeneous coordinates, put

A = r³ + 9r²s - rs² - s³, B = -4r(r²-s²).

We prove the exact identity A² + 2B² = F, where F is the homogeneous sextic. More strongly, for coprime r,s the common divisor of A and B divides eight. Thus after removing the forced parity factor the two conjugate factors are coprime away from the ramified prime above two. These are unconditional inputs to the fixed imaginary-quadratic descent, not a rational-point classification. This lower module also contains the direct rational-point transport from the original order-eighteen sextic. It stays independent of the later Eisenstein-cube correspondence so that the immutable X₁(18) challenge import can use these checked inputs without an import cycle.

The sextic on the anti-diagonal order-three quotient.

Equations
Instances For

    The degree-six homogeneous form attached to antiDiagonalSextic.

    Equations
    Instances For

      The real coefficient in the split quadratic norm.

      Equations
      Instances For

        The √-2 coefficient in the split quadratic norm.

        Equations
        Instances For

          The anti-diagonal quotient map #

          The denominator of the anti-diagonal invariant on the cubic correspondence.

          Equations
          Instances For

            The quadratic coefficient of the quotient equation.

            Equations
            Instances For

              The linear coefficient of the quotient equation.

              Equations
              Instances For

                The constant coefficient of the quotient equation.

                Equations
                Instances For

                  The square-root coordinate obtained from the discriminant of the quadratic quotient equation.

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

                    The exceptional polynomial forced by a zero quotient denominator.

                    Equations
                    Instances For

                      The homogeneous exceptional polynomial.

                      Equations
                      Instances For

                        The exceptional quotient-denominator polynomial has no rational root; the certificate is complete projective enumeration modulo five.

                        The exceptional denominator cannot vanish on a noncuspidal rational point of the cubic correspondence.

                        The discriminant of the quotient quadratic is nine times the anti-diagonal sextic.

                        theorem MazurTorsion.XOneEighteenDescent.antiDiagonal_quadratic_relation_identity (p q : ℚ) (hp0 : p ≠ 0) (hp1 : p ≠ 1) (hq0 : q ≠ 0) (hq1 : q ≠ 1) (hden : antiDiagonalDen p q ≠ 0) :

                        Exact rational-function identity producing the anti-diagonal quotient of the surviving cubic correspondence.

                        theorem MazurTorsion.XOneEighteenDescent.antiDiagonalZ_sq (p q : ℚ) (hp0 : p ≠ 0) (hp1 : p ≠ 1) (hq0 : q ≠ 0) (hq1 : q ≠ 1) (hden : antiDiagonalDen p q ≠ 0) (hcorrespondence : XOneEighteenFiniteField.invariantX p = 2 * XOneEighteenFiniteField.invariantX q - 6) :

                        A nondegenerate point of the cubic correspondence maps to the anti-diagonal genus-two curve.

                        The polynomial covariance identity underlying the Möbius comparison with the order-eighteen sextic already used by the Tate-normal-form consumer.

                        Rational-point transport from the order-eighteen model #

                        The Möbius coordinate carrying the order-eighteen sextic to the anti-diagonal model.

                        Equations
                        Instances For

                          The corresponding ordinate scaling on the order-eighteen sextic.

                          Equations
                          Instances For

                            The exceptional abscissa x = -1 cannot occur on the rational order-eighteen sextic.

                            The forward Möbius coordinate has the displayed rational inverse away from the exceptional abscissa.

                            The inverse-coordinate spelling of the sextic covariance identity.

                            Every rational point on the order-eighteen sextic maps, with the checked ordinate scaling, to a rational point on the anti-diagonal sextic.

                            A rational point on the original order-eighteen model supplies a nonexceptional anti-diagonal point together with the checked inverse abscissa. This is the point-level consumer of both Möbius identities.

                            Homogenizing at the canonical denominator recovers the integral sextic form.

                            First small Bézout identity for the two norm coefficients.

                            theorem MazurTorsion.XOneEighteenDescent.antiDiagonalNorm_bezout_den (r s : ℤ) :
                            (36 * r ^ 2 - 32 * s ^ 2) * antiDiagonalNormReal r s + (9 * r ^ 2 + 81 * r * s - 8 * s ^ 2) * antiDiagonalNormSqrtNegTwo r s = 32 * s ^ 5

                            Second small Bézout identity for the two norm coefficients.

                            For primitive homogeneous coordinates, the two coefficients of the quadratic norm have common divisor dividing eight.

                            The common divisor is exactly one for opposite parities and exactly eight for two odd primitive coordinates.

                            A primitive integral point on the anti-diagonal sextic supplies a quadratic norm equation whose two coefficients have gcd one or eight. This is the checked consumer of the factorization and support bound.

                            Every rational point on the anti-diagonal sextic has canonical primitive homogeneous coordinates satisfying the supported quadratic norm equation. This is the rational-point consumer used by the subsequent fixed-field square-class allocation.