Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2FirstPart1.Coefficients250To275

Recurrence 4 lookup certificate: Scalar2First coefficient convolution #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_250 :
Polynomial.coeff recurrence4Scalar2First 250 = (((2483186641565147251715274383 * 10 ^ 70 + 9904652045556734189150878180599517190429163029614959459219162518506732) * 10 ^ 70 + 2187222333976480949183726816109739911813132472688029023670898391607515) * 10 ^ 70 + 180784745912936916869859999740409278030332378103039760082716400160369) * 10 ^ 70 + 2670425594672462901875340292861405710033506987828824160459376709889807
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_251 :
Polynomial.coeff recurrence4Scalar2First 251 = -((((2311679209431065293336093060 * 10 ^ 70 + 3250186585865798096520242617543834145677146877113665335171051733500839) * 10 ^ 70 + 7811935272843574702842944288673455145428474215243158742598253724529426) * 10 ^ 70 + 7428545781597662959497485267561424554011643110625651359250428826086804) * 10 ^ 70 + 6813749522905959921678187969158523021695624511697877170201564151021769)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_252 :
Polynomial.coeff recurrence4Scalar2First 252 = (((2095730340095507393796124505 * 10 ^ 70 + 4743195381469383184825652124673983105949236828538796866302731498209747) * 10 ^ 70 + 6051942398160894904742857688731082434163111080074189995013935185713048) * 10 ^ 70 + 3866594944279616430554948060038730538767621542554076782500255723608517) * 10 ^ 70 + 1656576895273498330702273439294691787963634970492833824459736200825529
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_253 :
Polynomial.coeff recurrence4Scalar2First 253 = -((((1844067153169890630149986244 * 10 ^ 70 + 3882389629325284405237432254342048040953471082710431432019237376324286) * 10 ^ 70 + 4264661755048081387075882463297573653630694232989756671639905075820221) * 10 ^ 70 + 2038388352176552651213224066915122318027494521141431607230865896052752) * 10 ^ 70 + 3286445789471343574874122864923488197566455974071799123252503798257252)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_254 :
Polynomial.coeff recurrence4Scalar2First 254 = (((1567246228133543003919100022 * 10 ^ 70 + 2149691799500093545038359447090036928911593850557929887771274718051956) * 10 ^ 70 + 5149723275903267106903829600722775326722236836743822973692583306719276) * 10 ^ 70 + 2965658119846440000484045756161682361285468769803764659686019111823114) * 10 ^ 70 + 1649912637625772309365832878085736664967403291484195679428629677097640
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_255 :
Polynomial.coeff recurrence4Scalar2First 255 = -((((1276931010589789651842055236 * 10 ^ 70 + 479171070472380623539051295802912923653620999827970185435970744468860) * 10 ^ 70 + 1702210696080037554196436192916095504510812394609304397055039731063850) * 10 ^ 70 + 5713897234770260176339959242222689554989175607945148544983088633991979) * 10 ^ 70 + 4536962601718283450383902603489720244883240018033538014804416544386703)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_256 :
Polynomial.coeff recurrence4Scalar2First 256 = (((985084225056024638520809231 * 10 ^ 70 + 2271313158450585411568152651007592594944982717989905132584355080427544) * 10 ^ 70 + 6477261432977793328539984053469419129097685147299545719305552838676167) * 10 ^ 70 + 7825299447719078677447434543133072960609397495481232684495877824867338) * 10 ^ 70 + 3282043018438369482713134628192571149950258800293818384722244647745606
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_257 :
Polynomial.coeff recurrence4Scalar2First 257 = -((((703152567178671372170052520 * 10 ^ 70 + 4855970971986099519014209350868145685740120599581528974751650894619152) * 10 ^ 70 + 472576597729582865008267687525211583519245720313067140831879906644425) * 10 ^ 70 + 4292893682985752864659989063115946317874406131964197821898911720070469) * 10 ^ 70 + 526839742840883426587459996391837294027101537658338431323223058851349)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_258 :
Polynomial.coeff recurrence4Scalar2First 258 = (((441320877090571090823466739 * 10 ^ 70 + 7283248875338307746020096168600395147635385316139474933660417960696260) * 10 ^ 70 + 9158777421000283158243644236984040645812184484388346629085066413619296) * 10 ^ 70 + 5174343603625133461036290231777443530364924299062345685170638257722803) * 10 ^ 70 + 8223977702804683131258590324109893614250642067811064436670706921498781
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_259 :
Polynomial.coeff recurrence4Scalar2First 259 = -((((207903596584931773244845848 * 10 ^ 70 + 34263824408122562781847949342104827256964898316977197263447986354345) * 10 ^ 70 + 8460767313914204763785447000777222587301515279329909470248829229017510) * 10 ^ 70 + 4631116890410086162790160054234910781972294036387067410143329059695266) * 10 ^ 70 + 2370921002355630898000401719694673902851201750377325555955543007381513)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_260 :
Polynomial.coeff recurrence4Scalar2First 260 = (((8924016666771971420191081 * 10 ^ 70 + 7137954762097077093677822276618799824980942557727533883656241706614709) * 10 ^ 70 + 5852148346008852495337475157423361121394112222594116820650314021035939) * 10 ^ 70 + 1712263178979595328746458451558037209731840697522714880200386476825157) * 10 ^ 70 + 7363979060110780695997086994945476164115953777187908580410599440937423
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_261 :
Polynomial.coeff recurrence4Scalar2First 261 = (((152090820268225549849004529 * 10 ^ 70 + 6726532402529188667788982445573339314880143701972103340955281069739625) * 10 ^ 70 + 2815308410436165158687651151286941849103487485895518948829278544453024) * 10 ^ 70 + 1299060813816299547152612396720683606732719522895485446658840800936954) * 10 ^ 70 + 7037640242448620049689230301104024976499558055381315569502205594478569
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_262 :
Polynomial.coeff recurrence4Scalar2First 262 = -((((274096451083074214639733928 * 10 ^ 70 + 4166825390383653713105714577495273120639472471612484215843625966474442) * 10 ^ 70 + 3303072789863600752188528004197811712433503139935052371269767843232452) * 10 ^ 70 + 2980015833828475919906477090853769351742781122585058611044553975859187) * 10 ^ 70 + 5886440040245304797481770750573440766342966148546712642984116703879410)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_263 :
Polynomial.coeff recurrence4Scalar2First 263 = (((358318918455762389255792023 * 10 ^ 70 + 5290490223238527911852845246343538449535018641684111184146961816038855) * 10 ^ 70 + 1006825993840960108921351396674246098924833448787479754495140306731864) * 10 ^ 70 + 548048042312035182144628015092753388028041624690373824641285336194955) * 10 ^ 70 + 5707492464751418814646915243939416634076317962285876562809486041183855
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_264 :
Polynomial.coeff recurrence4Scalar2First 264 = -((((407883860536276594621680266 * 10 ^ 70 + 4348481691464602895704891711274500892931187729976816091925255577812164) * 10 ^ 70 + 84900497858759073238493533511106139962988484423120716944525378508966) * 10 ^ 70 + 1371425567072772799430270012311424342899737021315155922324156925771910) * 10 ^ 70 + 4237935112365267709798658825138389165905595614892782272300879123842351)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_265 :
Polynomial.coeff recurrence4Scalar2First 265 = (((427339100539127896299195705 * 10 ^ 70 + 9575294044806053290530341030997302685131202968398737358010922046007120) * 10 ^ 70 + 1488727090173753812633764470255134108165735259202863763703654669964467) * 10 ^ 70 + 5510753139631858173321302292192288583348214551676118297709683654414559) * 10 ^ 70 + 9325149516290828235838794173285047167072064069536130271668323118274627
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_266 :
Polynomial.coeff recurrence4Scalar2First 266 = -((((422128349864709602868525470 * 10 ^ 70 + 5515488201775807504171423476240498481215128020056176420065451620874315) * 10 ^ 70 + 5303896544954828949100039542145003387208325443233255256984014256962200) * 10 ^ 70 + 6066453712303901507296435178316791711755953035429522981038929856437800) * 10 ^ 70 + 7052244052917899147869466054329538297852382644498546607944935463040447)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_267 :
Polynomial.coeff recurrence4Scalar2First 267 = (((398071533721996033718153759 * 10 ^ 70 + 270625684209545003269848419954806190597805827309445653992366427481373) * 10 ^ 70 + 5329934155198310308533033783618293874253763316291824584814305860541332) * 10 ^ 70 + 7637435452327428058478765930678782172661316258759164307980592731657439) * 10 ^ 70 + 79975076915958621238880224398534578024890368330994871213315716805077
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_268 :
Polynomial.coeff recurrence4Scalar2First 268 = -((((360898908157625218893483134 * 10 ^ 70 + 9696248284724285988968666813806181572197534111447199780019008878920878) * 10 ^ 70 + 6568780022390875125036842544845597619601074559130967917562685349938626) * 10 ^ 70 + 7977357455469704397013772136967028914603995189355291203015424633809253) * 10 ^ 70 + 8744329407949443582950939141377535611595997837618206759814299939424880)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_269 :
Polynomial.coeff recurrence4Scalar2First 269 = (((315873449525649452155514331 * 10 ^ 70 + 1514558668117401006669506474645456407857468898069741588034665307668500) * 10 ^ 70 + 31009771355904396400487947865333985546226459997486440508286393666494) * 10 ^ 70 + 5322028019480101193321205756509621207268278912766736333989663014594030) * 10 ^ 70 + 148948306266678827967263014530837032888948078260579818822163631187025
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_270 :
Polynomial.coeff recurrence4Scalar2First 270 = -((((267521210120792349324739268 * 10 ^ 70 + 2451499573355673207751544452837510108464690253876295105960260247977669) * 10 ^ 70 + 4964555846791288703500417815475535729026911898537225570201976833569956) * 10 ^ 70 + 2566629217999244376327367071103328445461769547448897619694374644638386) * 10 ^ 70 + 5563276550321518473935289381856852529410308027292669954842319663485509)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_271 :
Polynomial.coeff recurrence4Scalar2First 271 = (((219474664592162343969963845 * 10 ^ 70 + 8163541154821863823655001490527271338223130515997227750161036260241011) * 10 ^ 70 + 3528478573007941710673215337467670450782597636575228205337540237958100) * 10 ^ 70 + 9283300663276587912303334959493383016929248084213747764386670368256756) * 10 ^ 70 + 4664860429992197303560706985303811121466159173754572548883900251015434
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_272 :
Polynomial.coeff recurrence4Scalar2First 272 = -((((174421376020690542791212217 * 10 ^ 70 + 2186485599690701989380790538939755555270311548836881922125141354809017) * 10 ^ 70 + 7583542656882667492471968222708975866931935636952881184431463501370814) * 10 ^ 70 + 6539153874046500630462764587993462797330372714448459063117155008989265) * 10 ^ 70 + 9941217355454440085516412306237284658365780954772150249253138669606833)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_273 :
Polynomial.coeff recurrence4Scalar2First 273 = (((134140858240025304817836588 * 10 ^ 70 + 3504939025743809285005745259365150683606487612341040528593363593249876) * 10 ^ 70 + 2978751330365749367620708774755821221700999185784310182331363067254267) * 10 ^ 70 + 1268087727669151100983006600252711133914548202279485978415234173415256) * 10 ^ 70 + 1664891880084667830211846028305697481277514346870741371998693999936219
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_274 :
Polynomial.coeff recurrence4Scalar2First 274 = -((((99606895467935773612379328 * 10 ^ 70 + 3564835048529717650266468633694884179217672284229908872399522657045800) * 10 ^ 70 + 7207139847157655906462649541033674180673377173721450930099284318561682) * 10 ^ 70 + 9669099742560586324506903188518024689960184283682617609364303477447109) * 10 ^ 70 + 4235916538258175657196289707206389139301204628030223747589684525752574)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_275 :
Polynomial.coeff recurrence4Scalar2First 275 = (((71130751899777849175712749 * 10 ^ 70 + 5908150399524763153230841258029962421148261967122996660915012272614746) * 10 ^ 70 + 6070867259794324552002262313490933318914141579749326699680230940512821) * 10 ^ 70 + 1879780190020929182825363819352051559852004597408301189266688439423754) * 10 ^ 70 + 3457449704130554139880668464580099009831970813242787907068629638904909