Recurrence 5 lookup certificate: Scalar1Second coefficient convolution #
This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_221 :
Polynomial.coeff recurrence5Scalar1Second 221 = ((((4627281395 * 10 ^ 70 + 4723996219364626995676320700991662822230715675149901164230467614130796) * 10 ^ 70 + 280924520358667790592523132416289928456006876418517386855508480513446) * 10 ^ 70 + 1323650855270747611222773069785741588300583504403408889125989909044814) * 10 ^ 70 + 8323879599044358650360775865786764161628689417538156211201918159784071) * 10 ^ 70 + 5989112637703649489351448645658714889713220765195851789903955946451385
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_222 :
Polynomial.coeff recurrence5Scalar1Second 222 = -(((((3780090621 * 10 ^ 70 + 4076661579460552379332291802481365452437562902866042281399029946711940) * 10 ^ 70 + 4736091619301323575730711456653088556531988583325155057380987472808335) * 10 ^ 70 + 3171051181920079358976507296838863701203356996092574844636033849580672) * 10 ^ 70 + 761752293602274645441160684031928849539702625552547191090370406321701) * 10 ^ 70 + 7563361583688297085796616088932104009140448767492063092557355161401051)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_223 :
Polynomial.coeff recurrence5Scalar1Second 223 = ((((3035520563 * 10 ^ 70 + 2130427222058795569991731004099159774966143134153440003168994099747866) * 10 ^ 70 + 1286242623041834096270128263099663381434433678628127678882513887334314) * 10 ^ 70 + 7301443907631646697849106695501768542383672433275820028119392389099277) * 10 ^ 70 + 9155485940676843610000562532624844165896011879081494363556746493495693) * 10 ^ 70 + 9124475682959874603851006434778679068430592571885820119368267126235555
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_224 :
Polynomial.coeff recurrence5Scalar1Second 224 = -(((((2395740850 * 10 ^ 70 + 6079990844641181488436871209874580370694353555709605634045247202600441) * 10 ^ 70 + 746007386627683873550883411721108124457470197456458536578579507898181) * 10 ^ 70 + 1104973521030855459500596024876555165245647739778993598393326466817809) * 10 ^ 70 + 6601934198875739011017757928744538533809715549869170041428796990789621) * 10 ^ 70 + 321757778697897028098762921716516429663085086016660262770215633087653)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_225 :
Polynomial.coeff recurrence5Scalar1Second 225 = ((((1857961575 * 10 ^ 70 + 1919623111778771604390104146127881955560946123121154554024310056180140) * 10 ^ 70 + 5615175672777269499176232735272763463349749943453694748318291122597174) * 10 ^ 70 + 1848527160724504890121436287483013257220485489536267692662268933471735) * 10 ^ 70 + 1027480008693710761067184267147868527869467041118788299454531063065508) * 10 ^ 70 + 8091811138041782969024072707561043085961929923259156817526082139944309
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_226 :
Polynomial.coeff recurrence5Scalar1Second 226 = -(((((1415576695 * 10 ^ 70 + 9818708736974207452112443482741890692202776005868641214659404962383252) * 10 ^ 70 + 6646657073502534420377195684133624364377602280084805599215203064111222) * 10 ^ 70 + 4327456001287888234659424999439142980652537524935073891407325994406999) * 10 ^ 70 + 4864768382542061571078296734962402997127377910539361528302241894106244) * 10 ^ 70 + 8931462627546867937342357713592046449295337696778077578532499680750267)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_227 :
Polynomial.coeff recurrence5Scalar1Second 227 = ((((1059343065 * 10 ^ 70 + 4581453702569377045136570543809325846394905396485729426027624755770558) * 10 ^ 70 + 6644206392531782240491454020487239051840615399779568368838101727128392) * 10 ^ 70 + 8363777381264241447758068045029038164667645220241961493487890138635236) * 10 ^ 70 + 2255585734632799573918092437053495185459572726184502983465993129384692) * 10 ^ 70 + 9310122259452754377919849560087265317120196892560948196096170578017661
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_228 :
Polynomial.coeff recurrence5Scalar1Second 228 = -(((((778490470 * 10 ^ 70 + 1592927181277409702650666075150578399818037909135702477240908267206918) * 10 ^ 70 + 3872734048078434077616641879883419928547273314080428207584342403279724) * 10 ^ 70 + 5324533365964463127829618594922980767825224248465259226719170480055428) * 10 ^ 70 + 4228695879295754137659147669471204584777574529013992163302865300524624) * 10 ^ 70 + 5976362027788227902295622615584219836519406903314250316851044085180221)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_229 :
Polynomial.coeff recurrence5Scalar1Second 229 = ((((561686627 * 10 ^ 70 + 4138571465355693427013183784346401224092145535360450773051314616554389) * 10 ^ 70 + 3148793102970270175610117303672558687800385997037303882625669072929507) * 10 ^ 70 + 8485898817024405371718718954426532336161902271858513998303208510659970) * 10 ^ 70 + 2866927966314755282633124454573563921034995108164617985678906046911040) * 10 ^ 70 + 2836380109413429127208674575080773427763116009258536384580918240402364
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_230 :
Polynomial.coeff recurrence5Scalar1Second 230 = -(((((397811529 * 10 ^ 70 + 2575719971829417382820695642247878855331917527197693934453385394189441) * 10 ^ 70 + 7538186223746160368969344098075533288638390965342331465750827302138470) * 10 ^ 70 + 3427419573852922597510511528144052941686887281650429044615344426041926) * 10 ^ 70 + 972537662390751299848594785282682345650339439040462706412777305308713) * 10 ^ 70 + 8349456261618034458922608532284986904258038414781624809502067436641745)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_231 :
Polynomial.coeff recurrence5Scalar1Second 231 = ((((276523902 * 10 ^ 70 + 1880998819256607129873422984408735625779502173798944421265899810653475) * 10 ^ 70 + 1001881082335877335757678654954730200786855982018488337272292029054697) * 10 ^ 70 + 3929020010411383788325052597741021310584272107746498764646525610797381) * 10 ^ 70 + 2872802655256458457982224164597834008101828667504782323485447043182020) * 10 ^ 70 + 221441975235432492752917731196090776087863144896031699340962394296287
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_232 :
Polynomial.coeff recurrence5Scalar1Second 232 = -(((((188626050 * 10 ^ 70 + 3269065665793287779578847392833035650470178916199446619296063233881694) * 10 ^ 70 + 4981157453164124685573717199092551424430711339209566486432090246851445) * 10 ^ 70 + 7696269444841470264779668050889893265049108251267798991789142374072043) * 10 ^ 70 + 1684443183684805937236985268829247349229801958704368330473246961887414) * 10 ^ 70 + 9087345355857015881037814112890462475010021515024463232869753090390775)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_233 :
Polynomial.coeff recurrence5Scalar1Second 233 = ((((126250438 * 10 ^ 70 + 9986895421064852688582480585693972806803803188324382427192411178969881) * 10 ^ 70 + 6485483369094503545741176606236824096289143094866270458332073027495278) * 10 ^ 70 + 9861368805025899977514758465771067820704616897210267447704997746182901) * 10 ^ 70 + 3647973039148291037302952098762368922547644065730586879482736743481106) * 10 ^ 70 + 9984236174651920361021402839301764496225599528955327099098667682061097
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_234 :
Polynomial.coeff recurrence5Scalar1Second 234 = -(((((82901697 * 10 ^ 70 + 4691112951295837338153214903107634340368977263501289884048905847208687) * 10 ^ 70 + 8467440607211641176594244931968256525471695460800686042710160594961833) * 10 ^ 70 + 4908523687245720126384746244736575082115973608548606904905083914056176) * 10 ^ 70 + 5534368690989217866297132335968494944274019018548538793711880843024462) * 10 ^ 70 + 922994185130910920101222738555507002517025470696981418377026305936651)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_235 :
Polynomial.coeff recurrence5Scalar1Second 235 = ((((53391841 * 10 ^ 70 + 9972363838326012373402086672167319646585541529977220167549657068143960) * 10 ^ 70 + 733652067083119226439073263108604514980722740345533490092681989597242) * 10 ^ 70 + 7027658337591083859521681897167419668677977388070740082467371955578375) * 10 ^ 70 + 6593250242405349225232373263843917944281174308451926947516678111047771) * 10 ^ 70 + 895141915211993135400326760919809146379187298841093563106818402888146
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_236 :
Polynomial.coeff recurrence5Scalar1Second 236 = -(((((33705624 * 10 ^ 70 + 7088457148822611464208389652829932810817403425437234935095904604485674) * 10 ^ 70 + 9757310891238375001976231533771191569480067433461385886497228061319525) * 10 ^ 70 + 8721513083514284270204948277333122004474279936278627680947726857392552) * 10 ^ 70 + 4095495021748077762156416964410281761809897251848410324501287229638246) * 10 ^ 70 + 2764639673163407487944761067009546470431311096008675715396553330426577)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_237 :
Polynomial.coeff recurrence5Scalar1Second 237 = ((((20828477 * 10 ^ 70 + 4960257733320825506852632277864623260137811594853869262078036869642011) * 10 ^ 70 + 3410538057682908585735327951631474202093951134974718545396982469548103) * 10 ^ 70 + 8959776540425367364452463009835544628965850214230350664785713950217093) * 10 ^ 70 + 2121567803525918448698657884220832609622724688325642241970483367755057) * 10 ^ 70 + 276057441157270388960750585196492198585354795523236167752268825212110
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_238 :
Polynomial.coeff recurrence5Scalar1Second 238 = -(((((12563044 * 10 ^ 70 + 4347702523130184044066418250979141740174474639411876917341106885092624) * 10 ^ 70 + 3121333116425372853100642875796916376287632082386018396066694328201290) * 10 ^ 70 + 4476994233612496934847005126772030740485457393186437549889152369768826) * 10 ^ 70 + 4346483705670229135097451404520791403414178136427993383457808669580094) * 10 ^ 70 + 8817041945716936197184267617776900892062199870135132543638803141995672)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_239 :
Polynomial.coeff recurrence5Scalar1Second 239 = ((((7353105 * 10 ^ 70 + 2518044848621377216721636717999680762536925039682370954308139262822987) * 10 ^ 70 + 6422916998180752797550391515557844488477354239806909454720940109036881) * 10 ^ 70 + 8535541319553283601664127596782133631285342815323542248900288219403937) * 10 ^ 70 + 9893238010211201466074240618194576190711787427331486690821934300215946) * 10 ^ 70 + 9705276010768446194581135189282569243420976947793334510320261132090870
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_240 :
Polynomial.coeff recurrence5Scalar1Second 240 = -(((((4126812 * 10 ^ 70 + 5058154788710736307804725215848070712259014389831790131008327840683900) * 10 ^ 70 + 1103722259997472097781841213746800922110064066651902332136083754276077) * 10 ^ 70 + 1121654832998477127857507074873518159436587587457695528550295074371144) * 10 ^ 70 + 2974319664924527522895235834023400251880489035551773015480052926254973) * 10 ^ 70 + 4083408783851964514754610828105098083809900831934928928391219914804484)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_241 :
Polynomial.coeff recurrence5Scalar1Second 241 = ((((2165278 * 10 ^ 70 + 7211453627359593293188569018988849805525564418237061317105535110157290) * 10 ^ 70 + 6787937184233002565680542665694997385529557906392962079290874512631213) * 10 ^ 70 + 1308419633824003579204151755833967447661098900454099589850529226454473) * 10 ^ 70 + 9473426861829418706084363488289615608351913600641787171892912756804458) * 10 ^ 70 + 6527500475352596823219316106559710474573207147535560447606806970509756
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_242 :
Polynomial.coeff recurrence5Scalar1Second 242 = -(((((998008 * 10 ^ 70 + 7287325593030876893268825586019768127248442626586703575909293561378871) * 10 ^ 70 + 808403058415687525518165651435130597695037449825292841605057397144923) * 10 ^ 70 + 7658988095440340487425262830121228882275950969825670905611050376256832) * 10 ^ 70 + 452396597921777883621726192527627960734536463920015084369583081763153) * 10 ^ 70 + 1305942646762688392669936281561373017702613243756633508932032649813625)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_243 :
Polynomial.coeff recurrence5Scalar1Second 243 = ((((323552 * 10 ^ 70 + 9891147855332790745993840764272413848909806353085685434788995310040241) * 10 ^ 70 + 4885690039709166768425878390989018181519185212110916240958565761247197) * 10 ^ 70 + 4423661221928680821497393162726986203874786181637179853459509398525816) * 10 ^ 70 + 5498844089958447204630292290346940073650011230639006976248331800778267) * 10 ^ 70 + 3589572406095535102056673058541995601762427531380791203183697321112925
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_244 :
Polynomial.coeff recurrence5Scalar1Second 244 = ((((48064 * 10 ^ 70 + 5014782653923872269452270619338746750319638614755436562083506480462992) * 10 ^ 70 + 5745385989843988728980150127574890129825530559220622467924263664972316) * 10 ^ 70 + 5607061363384219027951990714880238635678526162298481624998861061506784) * 10 ^ 70 + 6210456243068515556168020167583816577873818565067281696970801682739358) * 10 ^ 70 + 2662931425978397216016667027130728661976625660324695030872811020140394
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_245 :
Polynomial.coeff recurrence5Scalar1Second 245 = -(((((235359 * 10 ^ 70 + 3797205436558151976022831112714273133853144700573070483475013170846530) * 10 ^ 70 + 6069560679337163598244015245994675830248293605953409352745875834661558) * 10 ^ 70 + 4967428808982668853302186167868664578348266028189561678013245411352993) * 10 ^ 70 + 2672330608461672116553606084325258114001232242486999447964187675099760) * 10 ^ 70 + 4247428844058622550141913108197474124350476174392162000795723572696340)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_246 :
Polynomial.coeff recurrence5Scalar1Second 246 = ((((312066 * 10 ^ 70 + 7075274545928961109512494869599273684909287378391455976164237886320) * 10 ^ 70 + 6644779308524801630558107379971783593743743129945103059675103788501328) * 10 ^ 70 + 7852444265205483169219546639726639309954847886368765377612017231776951) * 10 ^ 70 + 9772322799139416349283533091558105305952484284339117291112316777036391) * 10 ^ 70 + 7552156311822427491294627240068694020258703996886557959468364186833438
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_247 :
Polynomial.coeff recurrence5Scalar1Second 247 = -(((((324242 * 10 ^ 70 + 591516385382489110859585575255513518090470142769305173943268816292174) * 10 ^ 70 + 171942491022854547566227951647222771757761637648535676106495958442960) * 10 ^ 70 + 675864921225054390686652469444330999747357368847874025746076098770835) * 10 ^ 70 + 3439440758736014687076993125540989442762079300067784881868742219550010) * 10 ^ 70 + 8459374010659810237125374778979181164282854412403249240842313834608928)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_248 :
Polynomial.coeff recurrence5Scalar1Second 248 = ((((300860 * 10 ^ 70 + 8461247266584051405145432840710033510954215996912898240231252799175336) * 10 ^ 70 + 2260743576863093104948394453863017647109494937678328841338836289838440) * 10 ^ 70 + 3406871138731786977507198752825537230266627297049279538787320004659937) * 10 ^ 70 + 3172524583736947371738032804473074160907260343501305469019786862152056) * 10 ^ 70 + 5943567109287943601827827300235928559588256946943936542660259148967424
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_249 :
Polynomial.coeff recurrence5Scalar1Second 249 = -(((((260204 * 10 ^ 70 + 1311794371339976782214558557742688563449244472542772524860185673500417) * 10 ^ 70 + 7386392368430309635399562476604410072705341583836711180148800601209047) * 10 ^ 70 + 9521109030816659098371569277532750809267285205491231606597651629956738) * 10 ^ 70 + 6465748213238055905027201236648513911958281533669551931303935540676468) * 10 ^ 70 + 8990373886030206351400070996241528768476930373444668877959629812006948)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_250 :
Polynomial.coeff recurrence5Scalar1Second 250 = ((((213684 * 10 ^ 70 + 5694661831580035404619180399471893500481673298844371592782331646411531) * 10 ^ 70 + 3086034167775778889514904352456806209645112837029955223918307057146470) * 10 ^ 70 + 2383659058271477243292448156453847723242485915297647442759575865711864) * 10 ^ 70 + 4630317170015056496780236537098259896908279135921093427011819105918954) * 10 ^ 70 + 6949838726154618346344049233537898309896514722175513785876952578643964