Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC0Low.Coefficients26To49

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_26 :
Polynomial.coeff remainder4Coefficient0 26 = 5358353641923289810316231454695640774731160930358869641301
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_27 :
Polynomial.coeff remainder4Coefficient0 27 = -151733892613902320668731059276185396977874583181787529963366
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_28 :
Polynomial.coeff remainder4Coefficient0 28 = 3916261660788291569420069376764028379928785109835567828887690
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_29 :
Polynomial.coeff remainder4Coefficient0 29 = -92448566200735918254424866746257832196092338994497115278176440
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_30 :
Polynomial.coeff remainder4Coefficient0 30 = 2002493030313663849759458446818828012981658913199308038612727636
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_31 :
Polynomial.coeff remainder4Coefficient0 31 = -39920648526267385629952858400090707042200265355834615164512062208
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_32 :
Polynomial.coeff remainder4Coefficient0 32 = 734533177819509477287413271955281502005821078427064188360344442371
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_33 :
Polynomial.coeff remainder4Coefficient0 33 = -12507452692977962651544595122820773459955498832237098200234945555742
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_34 :
Polynomial.coeff remainder4Coefficient0 34 = 197586420462991385248909542772129415135930036618213305292649025647133
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_35 :
Polynomial.coeff remainder4Coefficient0 35 = -2902680805118970352871139647271194747604401551075543746504464144683328
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_36 :
Polynomial.coeff remainder4Coefficient0 36 = 3 * 10 ^ 70 + 9742882462546483249549056718894116011316711210031170589579524649197846
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_37 :
Polynomial.coeff remainder4Coefficient0 37 = -(50 * 10 ^ 70 + 8213543483660942809957690511042854497063475878832254864470856856441634)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_38 :
Polynomial.coeff remainder4Coefficient0 38 = 608 * 10 ^ 70 + 1596189531773994598656774218130238755639278940312271766174398508850511
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_39 :
Polynomial.coeff remainder4Coefficient0 39 = -(6823 * 10 ^ 70 + 1251170549194221430846048959370653224910873577491003681983242674804801)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_40 :
Polynomial.coeff remainder4Coefficient0 40 = 71896 * 10 ^ 70 + 6819966711527633191319997714427672769795222442919773561069858031147343
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_41 :
Polynomial.coeff remainder4Coefficient0 41 = -(712718 * 10 ^ 70 + 734788483776173122298590248485379690068318915160677312771485795258676)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_42 :
Polynomial.coeff remainder4Coefficient0 42 = 6657247 * 10 ^ 70 + 6318226452339400055634241503321154514772743610266037296127378929400351
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_43 :
Polynomial.coeff remainder4Coefficient0 43 = -(58679670 * 10 ^ 70 + 1504962688268005975387631723641132508787499309238881208765493889823571)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_44 :
Polynomial.coeff remainder4Coefficient0 44 = 488776435 * 10 ^ 70 + 6956172415846479131359694355903840319106372781967595853558554161723593
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_45 :
Polynomial.coeff remainder4Coefficient0 45 = -(3852510585 * 10 ^ 70 + 8048473692569738347169218738352833697880681990998305810053119145127830)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_46 :
Polynomial.coeff remainder4Coefficient0 46 = 28769967559 * 10 ^ 70 + 9817819811918013130383649950126923852107816831092272538441039427590772
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_47 :
Polynomial.coeff remainder4Coefficient0 47 = -(203807058938 * 10 ^ 70 + 9069762039019664301648459371411587297439357768324093667918080645561781)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_48 :
Polynomial.coeff remainder4Coefficient0 48 = 1371130542823 * 10 ^ 70 + 1842150721098517967175393927491905839555583700223202166366631931175344
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C0_coeff_49 :
Polynomial.coeff remainder4Coefficient0 49 = -(8769768194628 * 10 ^ 70 + 9105807251357786741769827395230528932397345372402484534391047643844940)