Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingSelection

Polynomial selection for backtracking through the order-seven isogeny #

If Tate normalization of a point on the order-seven quotient produces the Fricke partner of the source parameter, clearing the two Hauptmodul expressions gives a polynomial equation. The raw equation depends on both affine coordinates. On the quotient curve, completed-square identities replace it by a compact polynomial depending only on the abscissa.

The final theorem packages the exact-order-49 consumer: the explicit Vélu image of such a point is not a kernel pole, lies on the quotient, and its abscissa satisfies the selection polynomial whenever the two Hauptmodul parameters agree.

source
def MazurTorsion.Kubert.orderSevenRawSelectionNumerator (d X Y : ℚ) :
ℚ

The raw cross-multiplied equation saying that the quotient point's level-seven Hauptmodul is the Fricke partner of the source parameter.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MazurTorsion.Kubert.orderSevenRawSelectionNumerator_eq_zero_of_hauptmodul_eq_fricke {d X Y : ℚ} [(orderSevenFamily d).IsElliptic] (h : orderSevenHauptmodulAt (orderSevenQuotient d) X Y = orderSevenFrickeParameter d) :
    orderSevenRawSelectionNumerator d X Y = 0

    Equality with the Fricke parameter forces the raw cleared selection equation.

    source
    def MazurTorsion.Kubert.pointTateCompletedTangentNumerator (W : WeierstrassCurve ℚ) (x : ℚ) :
    ℚ

    Twice the completed tangent numerator at an affine point.

    Equations
    Instances For
      source
      def MazurTorsion.Kubert.pointTateAlphaUnivariateCleared (W : WeierstrassCurve ℚ) (x : ℚ) :
      ℚ

      An abscissa-only cleared numerator for pointTateAlpha, rescaled by four on the curve.

      Equations
      Instances For
        source
        def MazurTorsion.Kubert.pointTateGammaUnivariateCleared (W : WeierstrassCurve ℚ) (x : ℚ) :
        ℚ

        An abscissa-only cleared last normalization factor, rescaled by four on the curve.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def MazurTorsion.Kubert.pointTateParameterUnivariateNumerator (W : WeierstrassCurve ℚ) (x : ℚ) :
          ℚ

          The abscissa-only numerator of the cleared Tate parameter.

          Equations
          Instances For
            source
            def MazurTorsion.Kubert.pointTateParameterUnivariateDenominator (W : WeierstrassCurve ℚ) (x : ℚ) :
            ℚ

            The abscissa-only denominator of the cleared Tate parameter.

            Equations
            Instances For
              source
              def MazurTorsion.Kubert.orderSevenSelectionPolynomial (d X : ℚ) :
              ℚ

              The compact abscissa-only selection polynomial on the order-seven quotient.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem MazurTorsion.Kubert.orderSevenSelectionPolynomial_eq_raw {d X Y : ℚ} (hcurve : (orderSevenQuotient d).toAffine.Equation X Y) :
                orderSevenSelectionPolynomial d X = 64 ^ 3 * orderSevenRawSelectionNumerator d X Y

                On the quotient curve, the abscissa-only selection polynomial is 64 ^ 3 times the raw cleared equation.

                source
                theorem MazurTorsion.Kubert.orderSevenSelectionPolynomial_eq_zero_of_hauptmodul_eq_fricke {d X Y : ℚ} [(orderSevenFamily d).IsElliptic] (hcurve : (orderSevenQuotient d).toAffine.Equation X Y) (h : orderSevenHauptmodulAt (orderSevenQuotient d) X Y = orderSevenFrickeParameter d) :
                orderSevenSelectionPolynomial d X = 0

                Fricke equality at a quotient point forces the compact selection polynomial to vanish at its abscissa.

                source
                theorem MazurTorsion.Kubert.orderSevenSelectionPolynomial_eq_zero_of_residual_eq_fricke {d x y : ℚ} [(orderSevenFamily d).IsElliptic] (hP : (orderSevenFamily d).toAffine.Nonsingular x y) (hQ : addOrderOf (WeierstrassCurve.Affine.Point.some x y hP) = 49) (h : orderSevenResidualHauptmodul d x y = orderSevenFrickeParameter d) :
                orderSevenSelectionPolynomial d (orderSevenVeluX d x) = 0

                Exact order 49 keeps a source point away from the order-seven kernel, so Fricke equality for its explicit Vélu image forces the compact selection polynomial to vanish.