Recurrence 4 lookup certificate: Scalar2Second 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.recurrence4Scalar2Second_coeff_217 :
Polynomial.coeff recurrence4Scalar2Second 217 = -((((898347868518803073014500 * 10 ^ 70 + 2546832504941276890535142544475411813484972618781760094506879929081838) * 10 ^ 70 + 581668792900033800749235122444873324179859166285919440468531081444544) * 10 ^ 70 + 5439567096339355952653525194266805580124082121971402612460700348291246) * 10 ^ 70 + 1780709927635232511036336761709174859636702683741547473136810323631617)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_218 :
Polynomial.coeff recurrence4Scalar2Second 218 = (((1385662994003916923652553 * 10 ^ 70 + 861716491857324266403708483120382727509450281121273240487643022954798) * 10 ^ 70 + 1825748560538336065620305177173770243054483048243363912095804692768164) * 10 ^ 70 + 8729123463520513904948545384459515188371850902979174463371459009104766) * 10 ^ 70 + 7401896140733610320203360638134903717510104200920795841113887098589524
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_219 :
Polynomial.coeff recurrence4Scalar2Second 219 = -((((2104171747663455788219039 * 10 ^ 70 + 1372839321062325235782756730401382885998708846825426636885465705559164) * 10 ^ 70 + 5826204591841512090541999159580959183632556625725223527078825783833682) * 10 ^ 70 + 3259649922238618566362527174773963493074773820474302963964444791267931) * 10 ^ 70 + 8442579377370833727531014027311412826039303063439171706489493184954762)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_220 :
Polynomial.coeff recurrence4Scalar2Second 220 = (((3145137576081187258740481 * 10 ^ 70 + 2027175747066700313892178028858054925547035819349064506752124321925353) * 10 ^ 70 + 7749298244337162741978387739159021773519522176011496303954056039419616) * 10 ^ 70 + 2334212702546438820789695644698967490953123061985957058177996880810185) * 10 ^ 70 + 8421346184176174145342229674404976334946211051313273626680169609305123
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_221 :
Polynomial.coeff recurrence4Scalar2Second 221 = -((((4626429498476710055103821 * 10 ^ 70 + 8796966160211058064075744729957166456677106433942041406814247875932942) * 10 ^ 70 + 7604035185770626829783214978082752231875391374619796828539746629312026) * 10 ^ 70 + 8586775864068231210820056370263356708108135176541342465572946164595130) * 10 ^ 70 + 7852483515245315036029088165956096033391886228444603082249652194256721)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_222 :
Polynomial.coeff recurrence4Scalar2Second 222 = (((6695752004413467958766979 * 10 ^ 70 + 1044349566296537220285761342490024091355842952145699735840956322188012) * 10 ^ 70 + 4913613500704930455419318673755779044777527051416179865992787364362995) * 10 ^ 70 + 204086564631565300775091918716940252472944485134040934173405758564337) * 10 ^ 70 + 7830421197565500040656456781056542166761711750821501451966406404589586
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_223 :
Polynomial.coeff recurrence4Scalar2Second 223 = -((((9531970490585233472022131 * 10 ^ 70 + 6442977420606888227245867379339330873608752650177439123024196126050182) * 10 ^ 70 + 1776913987857942529704307271026063773327166805319791729141223343516318) * 10 ^ 70 + 1165136301092725586234372715432453021814771391982839624204021275610620) * 10 ^ 70 + 7756229226165887953240921732511187560570733646451569959205430848328388)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_224 :
Polynomial.coeff recurrence4Scalar2Second 224 = (((13343160294238660504832867 * 10 ^ 70 + 6363716529992335584246732320371866387724082277453599217818215121917901) * 10 ^ 70 + 3619816394975664730768229711175059086458679745143137914693583634398070) * 10 ^ 70 + 8519829863509302596285448020441131447469159162402251063421879246736030) * 10 ^ 70 + 8545187437425863316515088725360451153707765140920459087901690212476431
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_225 :
Polynomial.coeff recurrence4Scalar2Second 225 = -((((18359696301951216206742413 * 10 ^ 70 + 8879765655414398734774050662880525252446370592029735862203577094712039) * 10 ^ 70 + 1277509087311848789460156440832738250648845350298524118113766570373962) * 10 ^ 70 + 3632457405954549463420541685020188079422221219562570420607513688356623) * 10 ^ 70 + 1240917268936149624984576294821496855509449325908592147799569388971679)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_226 :
Polynomial.coeff recurrence4Scalar2Second 226 = (((24820490995430949033246180 * 10 ^ 70 + 5941264801036246400196473598561033793477230633049539817494100498573643) * 10 ^ 70 + 2579869924690478239010575079432831552578557668973465549945492736148339) * 10 ^ 70 + 9504572684983317185228506035644485554434048422019522149802762842759613) * 10 ^ 70 + 8671433517033587629715787295469708887065424150062765355207869513515270
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_227 :
Polynomial.coeff recurrence4Scalar2Second 227 = -((((32950475981672660359788417 * 10 ^ 70 + 8413482359870367296237655791041854069959255517621351617719571186339293) * 10 ^ 70 + 3182880239169783869243053194850063566062175662702420564106548177789389) * 10 ^ 70 + 819118287048138638542028924647509660782914748103917032607983201756055) * 10 ^ 70 + 1434661085740380464053461639573778966714366332030193985566242361936674)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_228 :
Polynomial.coeff recurrence4Scalar2Second 228 = (((42927712812496522253221437 * 10 ^ 70 + 4041022748149003835228945578467063547993713435714476124447717390435520) * 10 ^ 70 + 8274333628404181592042929293744271442063479145403331974336639876295029) * 10 ^ 70 + 825094380104940963600258514064958270695572836397237711040795153350398) * 10 ^ 70 + 1542709523582967688249635371240514076837338072405532503572400677536240
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_229 :
Polynomial.coeff recurrence4Scalar2Second 229 = -((((54839217908201621896302436 * 10 ^ 70 + 1102416926349572559710814991284177697563325386015480971088186926562291) * 10 ^ 70 + 2158288354340999981732637692894505289178446408591815751362696579768774) * 10 ^ 70 + 2784277767663425879467758481051501810809019156178917980874137584489527) * 10 ^ 70 + 6081251521119379723469659446147726348216911856889759648768493704544406)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_230 :
Polynomial.coeff recurrence4Scalar2Second 230 = (((68625772822429545715140736 * 10 ^ 70 + 7171471468335273004449587529674276427253200008109300913338494314220225) * 10 ^ 70 + 7672920604813833695302009085185104878960288603769005098223150633854107) * 10 ^ 70 + 5682855681295658528426610980746442807314706071021080939779768182816085) * 10 ^ 70 + 1909515417024375283856006956332739790739449102508648714156553185413410
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_231 :
Polynomial.coeff recurrence4Scalar2Second 231 = -((((84017689912515009781305707 * 10 ^ 70 + 4258834773614367441272021782954254172242688498995503266113064347357634) * 10 ^ 70 + 3890070092296455013383197968855213136573587364615083643365447904432200) * 10 ^ 70 + 6862019125418056868221832404878008867963429504743032242531594306987698) * 10 ^ 70 + 2715410444194716550944457503362632754652987840564445898199098314342134)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_232 :
Polynomial.coeff recurrence4Scalar2Second 232 = (((100465655123681960789367887 * 10 ^ 70 + 9934556175899312919684083554858486024920400347598281307425417455870844) * 10 ^ 70 + 520753203393327688817398134926167374040319143447843201732465140934175) * 10 ^ 70 + 26796796837549557767189484289532349161239763747359415676151149534360) * 10 ^ 70 + 6837318515504249651508113338094716880348572308028254968827212181733304
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_233 :
Polynomial.coeff recurrence4Scalar2Second 233 = -((((117073203975932261849607332 * 10 ^ 70 + 8422645163874847496680410383754830479803254240824996411739198368099296) * 10 ^ 70 + 303611881293885047041776442550069080012627745534092229050609783028965) * 10 ^ 70 + 9998165496240275671859319754553050723213458924478186876709853591162682) * 10 ^ 70 + 4756809813739036291405588603906104799214335944783173868480077160432769)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_234 :
Polynomial.coeff recurrence4Scalar2Second 234 = (((132539809960375403997456798 * 10 ^ 70 + 4273426421020469745519464366143451254886406563005728107227383068912211) * 10 ^ 70 + 5131848608472775098499174092234457295025978841954127771234198090584426) * 10 ^ 70 + 4407881891871658777924335825127434941316226810183897369195801303314442) * 10 ^ 70 + 2080781706586247138274012587126278068658623249139844902639172277204425
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_235 :
Polynomial.coeff recurrence4Scalar2Second 235 = -((((145125565947528555077070026 * 10 ^ 70 + 68866350150436674421205815296084740602512860016751541468396501634929) * 10 ^ 70 + 5872913855535195673792545012252626987288918374534251789816126984006816) * 10 ^ 70 + 925512128027101115885113077585310099764323228452867633526076797883525) * 10 ^ 70 + 8127022067822646506041346857031303063200691641687487177188441571513630)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_236 :
Polynomial.coeff recurrence4Scalar2Second 236 = (((152649527116381706552789905 * 10 ^ 70 + 2068733478572527766667055952638939252779348248185686189032141959054614) * 10 ^ 70 + 2642187604623392272219647424195150389319163096976012206539178829116542) * 10 ^ 70 + 6195756421265731746942522294001953324762398388736785763505800847432454) * 10 ^ 70 + 5313707808635318550550443100293477256593200276227710626515461202314211
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_237 :
Polynomial.coeff recurrence4Scalar2Second 237 = -((((152533450935891103320964454 * 10 ^ 70 + 384699790798476596669357381243048869214999214536018361344902273586031) * 10 ^ 70 + 2569073061801728842008483798337623075099377131938313287325952828781318) * 10 ^ 70 + 7686966227505585531524104147585302671007125843363154594390601576821435) * 10 ^ 70 + 5976512721714654427443202863795616121586081454272734408760391720829023)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_238 :
Polynomial.coeff recurrence4Scalar2Second 238 = (((141900485655519552664965681 * 10 ^ 70 + 583987535045589109599534235052511004295989945609360128089916067328857) * 10 ^ 70 + 8804660720683058582455556869076131124832026737467581329241319968606335) * 10 ^ 70 + 1023876944410981176777324849117495045666778428455770570553608655684982) * 10 ^ 70 + 6279711775173886646688008218801709675571561710677866794204516491188155
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_239 :
Polynomial.coeff recurrence4Scalar2Second 239 = -((((117734079399049177659333315 * 10 ^ 70 + 2491266122851303771184532361498961734879467738234061019498311359361915) * 10 ^ 70 + 3017479682894132440671487574171973082155557142536974373288248085985360) * 10 ^ 70 + 1756417068503565294755484263373687081295872000149862337310821472471517) * 10 ^ 70 + 291927534941055565264596367457806307547944870347659645716301257797923)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_240 :
Polynomial.coeff recurrence4Scalar2Second 240 = (((77096055346362783712103612 * 10 ^ 70 + 4773272635724986758905036717479128922853170388160746761431980259574936) * 10 ^ 70 + 9795165989537087273762809139611341160166859057880902882163477013423552) * 10 ^ 70 + 7204154376970963491570982883541751186115690512936230266023958476981788) * 10 ^ 70 + 7859101739968822970722195323318499290765751609913502676193400489167264
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_241 :
Polynomial.coeff recurrence4Scalar2Second 241 = -((((17394844308470260331724164 * 10 ^ 70 + 8265723011706243502422601808345546344431731601174767110115356396228294) * 10 ^ 70 + 9537888432747970446576487758568966671486839456571633348172631836863139) * 10 ^ 70 + 8413743392896193697939074196302862013560320675753996099219683893524314) * 10 ^ 70 + 3471022733022214029012761323301460380446894100651628573495975250475446)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_242 :
Polynomial.coeff recurrence4Scalar2Second 242 = -((((63313897206107209041451620 * 10 ^ 70 + 3334759641962509538851333054533647945568580565823075542789092894293757) * 10 ^ 70 + 9716630282236244858905644722106692101312533729772557347591188028020297) * 10 ^ 70 + 1950888962128881338009316133088631726400803975505116134699268239902374) * 10 ^ 70 + 6814260923963390563029613436710730984791827049169673098192230195298627)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_243 :
Polynomial.coeff recurrence4Scalar2Second 243 = (((166020455846232333676605871 * 10 ^ 70 + 5081900227612218433018095744954691241156269091408801994097757902760339) * 10 ^ 70 + 6066896778671247820732158749671843348207995588679239056674323363159494) * 10 ^ 70 + 4972810917531703194285899222969921170434134136639998550419173285571253) * 10 ^ 70 + 3457686010101896628246216528501635844615458798639878944729734657751768