Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC0Low.Coefficients50To73

Recurrence 2 lookup certificate: C0 source coefficients, low half #

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_50 :
Polynomial.coeff remainder4Coefficient0 50 = 53381790827567 * 10 ^ 70 + 4244154274601007747366021648075638082852107911194677131652075737508590
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_51 :
Polynomial.coeff remainder4Coefficient0 51 = -(309540294753858 * 10 ^ 70 + 5033099372090542674237766588514053969279928818230534685864177133740893)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_52 :
Polynomial.coeff remainder4Coefficient0 52 = 1711441805490243 * 10 ^ 70 + 8397519695720582822022519525971149838281963279609161536387956405258181
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_53 :
Polynomial.coeff remainder4Coefficient0 53 = -(9030453049377010 * 10 ^ 70 + 3620101117270949708545493980196735893640531383917728158851069683150107)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_54 :
Polynomial.coeff remainder4Coefficient0 54 = 45511561886060662 * 10 ^ 70 + 8553333617391812603464342608246166234748804523050039435189284774870618
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_55 :
Polynomial.coeff remainder4Coefficient0 55 = -(219251642291040787 * 10 ^ 70 + 2546647733459784922820530093342100581728221553390189056035548213512656)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_56 :
Polynomial.coeff remainder4Coefficient0 56 = 1010414829029634936 * 10 ^ 70 + 2283908739166724087704574373383161256071197687769597165541031327709355
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_57 :
Polynomial.coeff remainder4Coefficient0 57 = -(4457616723382702318 * 10 ^ 70 + 8518894610137196556102341442606011929362970079119588195173611977297505)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_58 :
Polynomial.coeff remainder4Coefficient0 58 = 18838517245440986277 * 10 ^ 70 + 5320928688992881194800991872511702208729285651243929385941262443449604
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_59 :
Polynomial.coeff remainder4Coefficient0 59 = -(76315313516479787827 * 10 ^ 70 + 487081249516218809357606793885905185697080587464127738372814506070245)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_60 :
Polynomial.coeff remainder4Coefficient0 60 = 296526529348733163435 * 10 ^ 70 + 6514481098165307147414227312137481883543218630922227684358011914044149
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_61 :
Polynomial.coeff remainder4Coefficient0 61 = -(1105744495845591294834 * 10 ^ 70 + 3451132212385177366427028184281029405798960565992519866788614800313472)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_62 :
Polynomial.coeff remainder4Coefficient0 62 = 3959360916770984161287 * 10 ^ 70 + 5668367333964400645450168642981072450884470728478364009850981211642567
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_63 :
Polynomial.coeff remainder4Coefficient0 63 = -(13620780618649545980279 * 10 ^ 70 + 8469776891798179807115206150951316824482253717518633592867227313520635)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_64 :
Polynomial.coeff remainder4Coefficient0 64 = 45040315567274952965738 * 10 ^ 70 + 8294970071399877035643832432403887454354070337430932295112130830313719
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_65 :
Polynomial.coeff remainder4Coefficient0 65 = -(143228097551643054824078 * 10 ^ 70 + 7360685991333606995870890418040370088772968605232965571361190818481826)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_66 :
Polynomial.coeff remainder4Coefficient0 66 = 438204356006963667507926 * 10 ^ 70 + 1864273863292663309525678202294020243495815297457351575563856528955031
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_67 :
Polynomial.coeff remainder4Coefficient0 67 = -(1290419905869442014791300 * 10 ^ 70 + 2055337689149965597070498041553523859646916044207133608455447943182640)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_68 :
Polynomial.coeff remainder4Coefficient0 68 = 3659029743257642554173431 * 10 ^ 70 + 3703542967885994882804159830157614429159295750921710533045770572200706
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_69 :
Polynomial.coeff remainder4Coefficient0 69 = -(9994172003593366337249813 * 10 ^ 70 + 393434495052939879097110689110456733259243015996342669675310581726471)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_70 :
Polynomial.coeff remainder4Coefficient0 70 = 26304523612370033332620224 * 10 ^ 70 + 1222276478139228171605858045872634574646230975847957516258788819253348
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_71 :
Polynomial.coeff remainder4Coefficient0 71 = -(66736779679105242612865764 * 10 ^ 70 + 7397358923161793929807087608621757958188620872711622496208474733738499)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_72 :
Polynomial.coeff remainder4Coefficient0 72 = 163264507017518134829938958 * 10 ^ 70 + 6100282371851994185173758914013947766367631473503207541146652703706981
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_73 :
Polynomial.coeff remainder4Coefficient0 73 = -(385250397682266060202427579 * 10 ^ 70 + 7396905920202973374952255110301229417905034462509235067536187545336222)