Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC2Low.Coefficients0To47

Recurrence 2 lookup certificate: C2 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.recurrence2C2_coeff_0 :
Polynomial.coeff remainder4Coefficient2 0 = -64
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_1 :
Polynomial.coeff remainder4Coefficient2 1 = -2304332
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_2 :
Polynomial.coeff remainder4Coefficient2 2 = 4351552074
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_3 :
Polynomial.coeff remainder4Coefficient2 3 = 2049597779092
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_4 :
Polynomial.coeff remainder4Coefficient2 4 = -4556052408879169
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_5 :
Polynomial.coeff remainder4Coefficient2 5 = 874532532122652531
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_6 :
Polynomial.coeff remainder4Coefficient2 6 = 59446440182557909593
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_7 :
Polynomial.coeff remainder4Coefficient2 7 = -18502882904925888836011
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_8 :
Polynomial.coeff remainder4Coefficient2 8 = 4912385943209120888219118
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_9 :
Polynomial.coeff remainder4Coefficient2 9 = -2639045409644485295573372868
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_10 :
Polynomial.coeff remainder4Coefficient2 10 = 915986332852720437417728483863
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_11 :
Polynomial.coeff remainder4Coefficient2 11 = -230230871130867153443575699570114
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_12 :
Polynomial.coeff remainder4Coefficient2 12 = 45264993917586981432211305967416645
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_13 :
Polynomial.coeff remainder4Coefficient2 13 = -7177635900924328549827998262968343450
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_14 :
Polynomial.coeff remainder4Coefficient2 14 = 937489596749555104942542501054627067056
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_15 :
Polynomial.coeff remainder4Coefficient2 15 = -102537235566602929256870154653246146968996
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_16 :
Polynomial.coeff remainder4Coefficient2 16 = 9516497787927854908943043542644757562013819
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_17 :
Polynomial.coeff remainder4Coefficient2 17 = -757778993348436384828607781988592794232742478
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_18 :
Polynomial.coeff remainder4Coefficient2 18 = 52261032274217985515515946785123044449245519194
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_19 :
Polynomial.coeff remainder4Coefficient2 19 = -3147459571832016590123915681975513985686839897553
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_20 :
Polynomial.coeff remainder4Coefficient2 20 = 166745345552415934285180434377402371341850431455686
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_21 :
Polynomial.coeff remainder4Coefficient2 21 = -7821487084873965743785485852766728275897081978283045
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_22 :
Polynomial.coeff remainder4Coefficient2 22 = 326753883386574963909027413351757097790484310095062302
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_23 :
Polynomial.coeff remainder4Coefficient2 23 = -12222722310470569412386330677039986054254267809425800840
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_24 :
Polynomial.coeff remainder4Coefficient2 24 = 411386922754061508530848991732466558940850015096336542133
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_25 :
Polynomial.coeff remainder4Coefficient2 25 = -12514518301451981747490897816687493764383777762293189923117
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_26 :
Polynomial.coeff remainder4Coefficient2 26 = 345503400883236698909120295379973368672444877929995688065553
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_27 :
Polynomial.coeff remainder4Coefficient2 27 = -8690079482694159383495186147314633248071379744405240828821265
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_28 :
Polynomial.coeff remainder4Coefficient2 28 = 199832944043783648616752415312412166562677580938084751418105106
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_29 :
Polynomial.coeff remainder4Coefficient2 29 = -4215153552850333486976018580773660803425722159412792138801825559
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_30 :
Polynomial.coeff remainder4Coefficient2 30 = 81808171928975585462345479061177475364132915418493790665125735006
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_31 :
Polynomial.coeff remainder4Coefficient2 31 = -1465085524130665393471410606242097795431139616663159740506711353520
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_32 :
Polynomial.coeff remainder4Coefficient2 32 = 24276060177275660450661533255735744866863772927207302588938780068632
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_33 :
Polynomial.coeff remainder4Coefficient2 33 = -373108474151595088797085509708516268664083886217018733844471627411652
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_34 :
Polynomial.coeff remainder4Coefficient2 34 = 5331621480563295178346664345243197107509598408829027718310413009700835
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_35 :
Polynomial.coeff remainder4Coefficient2 35 = -(7 * 10 ^ 70 + 992854974766708070542941634942146886423648861751204543620501823485323)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_36 :
Polynomial.coeff remainder4Coefficient2 36 = 88 * 10 ^ 70 + 2689541031152503618183255663115435205937769017174569346850481750998813
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_37 :
Polynomial.coeff remainder4Coefficient2 37 = -(1026 * 10 ^ 70 + 8180563947718613862446603906791906599770392394356660756324728573630997)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_38 :
Polynomial.coeff remainder4Coefficient2 38 = 11196 * 10 ^ 70 + 3511290058583513763857217873521774935641030703934743551893562298962248
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_39 :
Polynomial.coeff remainder4Coefficient2 39 = -(114634 * 10 ^ 70 + 9269490689930531085774163938506065921542460294169656178465224116085207)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_40 :
Polynomial.coeff remainder4Coefficient2 40 = 1103907 * 10 ^ 70 + 1527243014212589557762745413691673747548615002205470576236836806867653
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_41 :
Polynomial.coeff remainder4Coefficient2 41 = -(10013862 * 10 ^ 70 + 429250878292738793251966595484855992510161222125863263008059593927708)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_42 :
Polynomial.coeff remainder4Coefficient2 42 = 85697012 * 10 ^ 70 + 9898858237764491910478462042142181285313995551730326039936847361552707
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_43 :
Polynomial.coeff remainder4Coefficient2 43 = -(692838407 * 10 ^ 70 + 2108573058237082493081576601393362221927092791863611155719242716850858)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_44 :
Polynomial.coeff remainder4Coefficient2 44 = 5298773666 * 10 ^ 70 + 2964008295645781653987743253557955527605415918039609157178066771212689
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_45 :
Polynomial.coeff remainder4Coefficient2 45 = -(38383155575 * 10 ^ 70 + 8588257394069248908014392420750440878730775187456836094839513814671876)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_46 :
Polynomial.coeff remainder4Coefficient2 46 = 263660005580 * 10 ^ 70 + 2097803164475023877498218048342576236187708099368663392249242719952462
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C2_coeff_47 :
Polynomial.coeff remainder4Coefficient2 47 = -(1719395647171 * 10 ^ 70 + 2731370699530723262595222805039125853183824652363809323964862661291784)