Recurrence 4 lookup certificate: Scalar1Exceptional coefficient convolution #
This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_205 :
Polynomial.coeff recurrence4Scalar1Exceptional 205 = -((((96324750254617888378 * 10 ^ 70 + 1398623071739271581742596690625803252924011889464512957483905986166797) * 10 ^ 70 + 3210891456806621694124543358438658300924853396940608417676726117244020) * 10 ^ 70 + 5471556109831502042406026474438563702795359445712710100811204058773632) * 10 ^ 70 + 37888253263080824799061595775109381866566821347059401139272059478514)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_206 :
Polynomial.coeff recurrence4Scalar1Exceptional 206 = (((194491404210799357801 * 10 ^ 70 + 1824225426491771030744984949996002838647985784702023507112484021412938) * 10 ^ 70 + 30449716456642657501313944533139086320735245782628831014584758359226) * 10 ^ 70 + 1258381873528626706149292095970998252855307601387295540010468060374238) * 10 ^ 70 + 351178997996333848496874199781924963957919165551956292231930974942172
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_207 :
Polynomial.coeff recurrence4Scalar1Exceptional 207 = -((((387168414651344971576 * 10 ^ 70 + 9964078610019737547956581355036540448559933601251110797014284264412613) * 10 ^ 70 + 654867312580059604152582127231545130323359271118084640517168495367927) * 10 ^ 70 + 3392503992040551706778276655056597943937081777713300078066322017591723) * 10 ^ 70 + 1195658242635801966817393280464803198593442784340755423060135510757883)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_208 :
Polynomial.coeff recurrence4Scalar1Exceptional 208 = (((759904313915260319701 * 10 ^ 70 + 5678928573076803688718554041098394995716636631235726531482404994293483) * 10 ^ 70 + 8719939490129543680086220010387619825240006891642424396085475192424800) * 10 ^ 70 + 911687720496325481143456236622514983314553512798849385303890007090813) * 10 ^ 70 + 5100855609246072677138067471727361503162686537185930912976330379997211
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_209 :
Polynomial.coeff recurrence4Scalar1Exceptional 209 = -((((1470615497181496186087 * 10 ^ 70 + 3724373144448858785897331069043505868846186053457545720510545791018147) * 10 ^ 70 + 8724129565229792345454879789039837944169601013851785105027743953313279) * 10 ^ 70 + 8124797898976951405289168601292107216419282232781191319693808889494665) * 10 ^ 70 + 5833825951404422752743695221478716978178234917330785158274994581554719)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_210 :
Polynomial.coeff recurrence4Scalar1Exceptional 210 = (((2806348816550092411556 * 10 ^ 70 + 8640322757547995538409518603639799564356403090621098781331390134100406) * 10 ^ 70 + 888451133293732626763613645938399750417179215616514647907903140135732) * 10 ^ 70 + 3313132208874504531551772262380297452972693045088112785276004500964054) * 10 ^ 70 + 786375079732146943914491659147300024194057134042910884739626300086422
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_211 :
Polynomial.coeff recurrence4Scalar1Exceptional 211 = -((((5280886180889498999118 * 10 ^ 70 + 2067413528483802303654345540228180087135087548244011836928963537596149) * 10 ^ 70 + 8476641430920708066249122694568913270072350892976522665283325297989954) * 10 ^ 70 + 834650106137404233968273837688348147213768220080216879733268623887221) * 10 ^ 70 + 4392832553758677673938238550969467610392170729204156415324009146570988)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_212 :
Polynomial.coeff recurrence4Scalar1Exceptional 212 = (((9799734325393452126808 * 10 ^ 70 + 9559165389209132968574577587556126268132623113996863822433191882905975) * 10 ^ 70 + 921212604376194914636470821362470991112872356498789112903430948814006) * 10 ^ 70 + 5646854673994312610416465526317018966754372911002326922621312049181709) * 10 ^ 70 + 5774414279441461739591167210306409726008503974607241312471874076262634
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_213 :
Polynomial.coeff recurrence4Scalar1Exceptional 213 = -((((17934248639367832298278 * 10 ^ 70 + 9737288329613467125267252828634820253228443284422279899516621981520153) * 10 ^ 70 + 8059861382916615685422075797213825947685383084858006496385078484450681) * 10 ^ 70 + 7856536149913019948944504800145570551661064558493175090488245410840614) * 10 ^ 70 + 816774845832859783388139320394390163800822134479544371390867459937143)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_214 :
Polynomial.coeff recurrence4Scalar1Exceptional 214 = (((32369194226759684340563 * 10 ^ 70 + 8490316101151874613017660584089797145032747958410789241056703412262722) * 10 ^ 70 + 76014355855964643942328435571447498130710958748487032934631579231032) * 10 ^ 70 + 5489661056585800091298701144951235341033773693598015824363847349134417) * 10 ^ 70 + 6528310107702412433043780826831328131183741716809116679793824143788737
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_215 :
Polynomial.coeff recurrence4Scalar1Exceptional 215 = -((((57620660284139169200772 * 10 ^ 70 + 7125730493552030751366194659878324436126929001060011829962724016384399) * 10 ^ 70 + 4263127449883106747887496818557611503703162400954705922089947965780497) * 10 ^ 70 + 5910874300690728151562688647678231941319825098662291667381533877253556) * 10 ^ 70 + 5102349858436420673470189449911780948081100062325982577596040815578547)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_216 :
Polynomial.coeff recurrence4Scalar1Exceptional 216 = (((101167134103616419335421 * 10 ^ 70 + 2524059696239456485136256980289439706253004733120007682850916849777903) * 10 ^ 70 + 7926387751137541814790785051083956977395858491871131520432310860221478) * 10 ^ 70 + 6728330211306531925126823909712178737065748875272253761493578494107764) * 10 ^ 70 + 5241901184784060113686528505381052475472552981975421547255882877844880
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_217 :
Polynomial.coeff recurrence4Scalar1Exceptional 217 = -((((175199233471222422856627 * 10 ^ 70 + 7014241772610281957855933914454931648734666699426051982068788602801122) * 10 ^ 70 + 4155820289379318718701474120814626089610839026939204031820034768574964) * 10 ^ 70 + 5043857986292364264429711734122909122086967386480626161635619753432537) * 10 ^ 70 + 8375197832517323630779416901602195190383914867067067392660808530368992)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_218 :
Polynomial.coeff recurrence4Scalar1Exceptional 218 = (((299276489226790133963937 * 10 ^ 70 + 3462024965798872762292631214164445904963238784882066053618081966083993) * 10 ^ 70 + 5976353090561391084282124407547598349649834740019531872967038457502026) * 10 ^ 70 + 1992197487818191659504397181454660057928974743981584100634508295510503) * 10 ^ 70 + 2192622298267228754129868122643908092883089023501057453931914829206603
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_219 :
Polynomial.coeff recurrence4Scalar1Exceptional 219 = -((((504285184143773126023247 * 10 ^ 70 + 61903825369897690450925923790026560876993744128798534559211955909122) * 10 ^ 70 + 4867908995099174051667743878082870901828340415925136863098637717539103) * 10 ^ 70 + 6898591735636992181429177945990912051432708832838490549491101488174960) * 10 ^ 70 + 5455235982427463644943714333141399850827170214401571327219110453106886)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_220 :
Polynomial.coeff recurrence4Scalar1Exceptional 220 = (((838220085263149028473527 * 10 ^ 70 + 2202833312653911100022583025206816184801717765333337206496084530418920) * 10 ^ 70 + 4734454833338924849360987475406058365752600503325778214491272323354403) * 10 ^ 70 + 9805890667867994308568353562128296512492213565295431429166457258766846) * 10 ^ 70 + 6878559806065884553916541151740267069243104559976418688573484007137032
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_221 :
Polynomial.coeff recurrence4Scalar1Exceptional 221 = -((((1374461833114874632099671 * 10 ^ 70 + 2580170820153760555308569969430390073585714659300239009022954076688831) * 10 ^ 70 + 4087346578022442703693978993929339954650386059280340484806423799256731) * 10 ^ 70 + 7513690768801700001994460445880832572351815883227772258505489008084626) * 10 ^ 70 + 2457410995881205786582890649997523466205487254353123095311930245511544)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_222 :
Polynomial.coeff recurrence4Scalar1Exceptional 222 = (((2223382028761583887693998 * 10 ^ 70 + 3448891320840507047230257974981616939029173825989676489105419795171266) * 10 ^ 70 + 1979129469870399279205537105287185617733726519117758219119380842495603) * 10 ^ 70 + 5053863449174701754108340219722084922350734295040117689916063597677242) * 10 ^ 70 + 2273368673130746694251712682395167675514975742765831787937020642952416
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_223 :
Polynomial.coeff recurrence4Scalar1Exceptional 223 = -((((3548263043717062662890375 * 10 ^ 70 + 8319492357045707089640898956708586423970693995574410209282642123007272) * 10 ^ 70 + 1400250263047121296317838982150096803303666328982336828695021048703192) * 10 ^ 70 + 4262746227149355227143097512205375518462447184527856087938722027476820) * 10 ^ 70 + 3087671800027156677863624177248794453955139449726610133852951463243548)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_224 :
Polynomial.coeff recurrence4Scalar1Exceptional 224 = (((5586642483559472716473929 * 10 ^ 70 + 8935324613463845396479635634000256294405941448879596422174206375376814) * 10 ^ 70 + 4997224377212303240264034250921230318968927774109761052436033490519216) * 10 ^ 70 + 4076237641367664208127460493991176439816882117219873705933569387034825) * 10 ^ 70 + 1074506073141509786972589890447521157420412427092337140246276480155163
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_225 :
Polynomial.coeff recurrence4Scalar1Exceptional 225 = -((((8678244444709577090063424 * 10 ^ 70 + 4801116710040842533957541132427907280985726460128605774200158620043683) * 10 ^ 70 + 9811255778538856061889058080912967567618992217656071656203736802130672) * 10 ^ 70 + 5470302767224621992099153111212976772445939493142347324405109836057906) * 10 ^ 70 + 4982381818980317899294216452457805843047965847279781081040052991625798)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_226 :
Polynomial.coeff recurrence4Scalar1Exceptional 226 = (((13300590331285146684722131 * 10 ^ 70 + 4507569952261269512356436089797636752505356220649039871977457812092776) * 10 ^ 70 + 9627285123888756248234494325544097784822728740179904514726130301224820) * 10 ^ 70 + 1828660603036536345778599333139787301598155097878694707842872109559170) * 10 ^ 70 + 7492300440143480564794233675754238957466305764724799234515857254938214