Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingSymmetry

Order-three symmetry of the order-seven backtracking cofactors #

The fractional-linear parameter transformation d ↦ 1 / (1 - d) cyclically permutes the three canonical degree-seven division cofactors and preserves the selection cofactor up to scale. The accompanying affine change of the polynomial variable is explicit, so a coprimality certificate for one division cofactor can be transported to the other two.

The division identities check the stored coefficient tables directly. The selection identity instead transports the structural Tate and dual-kernel factorizations, then cancels their certified common factor.

source
def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.orderThreeParameter (d : ℚ) :
ℚ

The order-three transformation of the order-seven Hauptmodul parameter.

Equations
Instances For
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.orderThreeAffine (d : ℚ) :
    Polynomial ℚ

    The affine polynomial-variable change accompanying orderThreeParameter.

    Equations
    Instances For
      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.orderThreeParameter_ne_zero (d : ℚ) (hd : d ≠ 1) :
      orderThreeParameter d ≠ 0

      The order-three transform stays away from zero when the original parameter stays away from one.

      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.orderThreeParameter_ne_one (d : ℚ) (hd : d ≠ 0) :
      orderThreeParameter d ≠ 1

      The order-three transform stays away from one when the original parameter stays away from zero.

      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.discriminantFactor_orderThreeParameter (d : ℚ) (hd : d ≠ 1) :
      orderThreeParameter d ^ 3 - 8 * orderThreeParameter d ^ 2 + 5 * orderThreeParameter d + 1 = (d - 1)⁻¹ ^ 3 * (d ^ 3 - 8 * d ^ 2 + 5 * d + 1)

      The cubic singular factor is preserved up to a nonzero cube by the order-three parameter symmetry.

      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.divisionCofactor0_orderThreeParameter_comp (d : ℚ) (hd : d ≠ 1) :
      (divisionCofactor0 (orderThreeParameter d)).comp (orderThreeAffine d) = Polynomial.C ((d - 1)⁻¹ ^ 28) * divisionCofactor1 d

      The order-three parameter symmetry sends the first division cofactor to the second.

      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.divisionCofactor1_orderThreeParameter_comp (d : ℚ) (hd : d ≠ 1) :
      (divisionCofactor1 (orderThreeParameter d)).comp (orderThreeAffine d) = Polynomial.C ((d - 1)⁻¹ ^ 28) * divisionCofactor2 d

      The order-three parameter symmetry sends the second division cofactor to the third.

      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.divisionCofactor2_orderThreeParameter_comp (d : ℚ) (hd : d ≠ 1) :
      (divisionCofactor2 (orderThreeParameter d)).comp (orderThreeAffine d) = Polynomial.C ((d - 1)⁻¹ ^ 28) * divisionCofactor0 d

      The order-three parameter symmetry sends the third division cofactor back to the first.

      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.selectionCofactor_orderThreeParameter_comp (d : ℚ) (hd : d ≠ 1) :
      (selectionCofactor (orderThreeParameter d)).comp (orderThreeAffine d) = Polynomial.C ((d - 1)⁻¹ ^ 135) * selectionCofactor d

      The selection cofactor is preserved up to scale by the order-three parameter symmetry.

      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.isCoprime_selection_divisionCofactor1_of_orderThreeParameter (d : ℚ) (hd : d ≠ 1) (hcop : IsCoprime (selectionCofactor (orderThreeParameter d)) (divisionCofactor0 (orderThreeParameter d))) :
      IsCoprime (selectionCofactor d) (divisionCofactor1 d)

      Coprimality with the first division cofactor at the transformed parameter transports to coprimality with the second cofactor.

      source
      theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.isCoprime_selection_divisionCofactor2_of_orderThreeParameter (d : ℚ) (hd : d ≠ 1) (hcop : IsCoprime (selectionCofactor (orderThreeParameter d)) (divisionCofactor1 (orderThreeParameter d))) :
      IsCoprime (selectionCofactor d) (divisionCofactor2 d)

      Coprimality with the second division cofactor at the transformed parameter transports to coprimality with the third cofactor.