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_244 :
Polynomial.coeff recurrence4Scalar2Second 244 = -((((290480830804459480945177706 * 10 ^ 70 + 1679346845719439212256651613538876409940863691425261210358102707436272) * 10 ^ 70 + 4448555188901957397335469099326816449649069789179214801500148928803434) * 10 ^ 70 + 1979109193244092962348342335814913452752714254281790923348175325192324) * 10 ^ 70 + 9360489831026473152966642799449650540074353078246047812546870729692263)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_245 :
Polynomial.coeff recurrence4Scalar2Second 245 = (((434999381976932099151541258 * 10 ^ 70 + 593997680892914799664878554337101759717497627209696594559340797902338) * 10 ^ 70 + 6886102036896952252365895933136805952017456734724833600809037001487615) * 10 ^ 70 + 2007011484949108111657586312054671242070047247127685494176533176264391) * 10 ^ 70 + 6904172866098410733329650661677535710130985325786716725649248471272392
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_246 :
Polynomial.coeff recurrence4Scalar2Second 246 = -((((596309740078717068084273635 * 10 ^ 70 + 3951717016470297869848372476821420512564451964585397888473225445940868) * 10 ^ 70 + 2297278110241762447569095777594693056966749701507605442033092597877974) * 10 ^ 70 + 7678140377456723044963789831028526937565581284663798283250800239079568) * 10 ^ 70 + 7269698062065271711713944717848832626915859934648420110829941553493992)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_247 :
Polynomial.coeff recurrence4Scalar2Second 247 = (((769583420800223511262768168 * 10 ^ 70 + 6008840419450882197559814715005745264060673611193553331076451040293406) * 10 ^ 70 + 314314105671109707314948613576431136811243256562074992689241471172693) * 10 ^ 70 + 6417655775417550223122693021940398602685367025990563762131696666265602) * 10 ^ 70 + 7902365788259363338296976044238635060764779089369735696398268405879354
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_248 :
Polynomial.coeff recurrence4Scalar2Second 248 = -((((948584625598239398509913012 * 10 ^ 70 + 7392538295698692990654425938067225885143466620669090692722430984458872) * 10 ^ 70 + 6768551068814079594177878478585956007014483788245771921277228198324621) * 10 ^ 70 + 8999078527857957319087330745010376204368607035618351853251486287211002) * 10 ^ 70 + 5187178228828434311877219198239320580554268535899247924941364304536452)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_249 :
Polynomial.coeff recurrence4Scalar2Second 249 = (((1125974593519099614233541666 * 10 ^ 70 + 2278616896075037626173804052402508118719270333459568761192378113008817) * 10 ^ 70 + 3170012394482966723802124184689617006742633775843391606212817274561761) * 10 ^ 70 + 7815828663331646584715829365666116837616456062715769531306505110654297) * 10 ^ 70 + 1819403847657647250632352210752405744859031990910362636974067440626224
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_250 :
Polynomial.coeff recurrence4Scalar2Second 250 = -((((1293751260788872420216882193 * 10 ^ 70 + 6530050065336562826339082317488904615793990745440397805124067474557157) * 10 ^ 70 + 692948239765816136309412307512158147461048909356089191517642787201735) * 10 ^ 70 + 6079920528452422651338088475856340894394416259086434692359129014131147) * 10 ^ 70 + 7299840119080854428913536330118394918215802429776599343788624389806313)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_251 :
Polynomial.coeff recurrence4Scalar2Second 251 = (((1443792186039145153901749298 * 10 ^ 70 + 1642826614663998455493556620608718603889271365292278611519095375825178) * 10 ^ 70 + 6565238321307304100331225945755243976130454090745474784988438061304820) * 10 ^ 70 + 5974155709497861404667590969594105238078574508217778674165932537887553) * 10 ^ 70 + 5345289746642570405521431208262327261635369491297493370687833917881580
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_252 :
Polynomial.coeff recurrence4Scalar2Second 252 = -((((1568453312105850328390915928 * 10 ^ 70 + 8757976170559150169324260860598238173873859422847343465470614863062165) * 10 ^ 70 + 7926438090726304493830193760550641687720392192809050824069289451049480) * 10 ^ 70 + 9864663520620649525730228194670839966015668439946248180850335871141912) * 10 ^ 70 + 4603464782949445670571155360773681626538029509651401391532579131791629)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_253 :
Polynomial.coeff recurrence4Scalar2Second 253 = (((1661165647990363939937008065 * 10 ^ 70 + 2923723255290435618076582941409337667595642841395772624648344745011836) * 10 ^ 70 + 8529772222289974735516809012154901859524837404903373314673451332512285) * 10 ^ 70 + 6338782176278388270574587564346002872474777056314971839395384829978388) * 10 ^ 70 + 1159181524530408580009300934611729153309432788381248781470469728591800
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_254 :
Polynomial.coeff recurrence4Scalar2Second 254 = -((((1716968296175243830668618467 * 10 ^ 70 + 286640286342367818011551306810484862268276312737217520914680952722403) * 10 ^ 70 + 9666954262887528284049577536135788403452836373847093486596288829775126) * 10 ^ 70 + 8535426818404721781521583391819625463714633019551485652184496478968266) * 10 ^ 70 + 2354850075439523806471664037820078319425109643226895315668319295993829)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_255 :
Polynomial.coeff recurrence4Scalar2Second 255 = (((1732920413287398286266609754 * 10 ^ 70 + 1327994549115458041495148324970423989262912152120080306797123136803482) * 10 ^ 70 + 271093711685760756218099354947650201985202338044299620213445615611439) * 10 ^ 70 + 6832682418163508716974722078795488556875041428819875681066873702592962) * 10 ^ 70 + 3434288011047150684921517839070027892688347862980559036285065446919618
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_256 :
Polynomial.coeff recurrence4Scalar2Second 256 = -((((1708346496969869761431297238 * 10 ^ 70 + 8241498523992013142105309867898249633603298787890991222357097913209628) * 10 ^ 70 + 4634878228353878817342380904739565005150149747163135578058120743827784) * 10 ^ 70 + 8423878697952008919877608429530651719816468317444916416484958744394312) * 10 ^ 70 + 2208517682432398221676713197192867520811291827832210352771281970845818)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_257 :
Polynomial.coeff recurrence4Scalar2Second 257 = (((1644887454909533140452847969 * 10 ^ 70 + 6413676651152469252798103176017472639962897478931598206477133732327175) * 10 ^ 70 + 2928955383656469692400931817512995653743130292862482199288996060716146) * 10 ^ 70 + 6626135996583633913929415852280866042942177788374674135510229228577055) * 10 ^ 70 + 2561245963848492755823074433911789558614118941802263649202916565343612
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_258 :
Polynomial.coeff recurrence4Scalar2Second 258 = -((((1546351829959106466478821213 * 10 ^ 70 + 5114736390367526503935432549443570522691625393596855003478936744542528) * 10 ^ 70 + 1874026094276530613223037946954901542870881520471365202812778057188242) * 10 ^ 70 + 4329513180253008644738718368288078145905370613799061937959263060677580) * 10 ^ 70 + 967083885852469581357398042466073590213780338618285205929655706269837)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_259 :
Polynomial.coeff recurrence4Scalar2Second 259 = (((1418384282241222260374349369 * 10 ^ 70 + 1943230517132771813172849812863054360923107469508642360750796904841697) * 10 ^ 70 + 827705918325918411823167337130920708100905820329127928298004268662385) * 10 ^ 70 + 4831405931096851353985041794233272793480256881597977131811969789722367) * 10 ^ 70 + 7164372440505090707341198486611315163803049373639914416399669608368963
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_260 :
Polynomial.coeff recurrence4Scalar2Second 260 = -((((1267988777132831172449674944 * 10 ^ 70 + 8692961897802132260152964029771442158124845154394548716294581013921679) * 10 ^ 70 + 429582028010903236156487668245110835775085483921327265788764208452951) * 10 ^ 70 + 897042725421397667953143978644413033105306558709224426683691778488350) * 10 ^ 70 + 5750382358239314520503036559570046585563764146115047353369799710845212)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_261 :
Polynomial.coeff recurrence4Scalar2Second 261 = (((1102959097058281122069150795 * 10 ^ 70 + 5455371553277452374673568006358510373587404646710888962564211866878499) * 10 ^ 70 + 2132024116757600111472529307601705069556535412803573104633435543260823) * 10 ^ 70 + 949266063732364117006549942379745350146629689848344869795554925841387) * 10 ^ 70 + 6382035345827136700723563279077829753382244311906833313293739737545291
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_262 :
Polynomial.coeff recurrence4Scalar2Second 262 = -((((931277330288171622912019006 * 10 ^ 70 + 1967854856560142683434131807260765944806660951249377603991411089813546) * 10 ^ 70 + 479248339419425419098627379264404067991990210526712323593149684613158) * 10 ^ 70 + 8243306205239279610852214499446486483717226040938554372348585301860024) * 10 ^ 70 + 8258713140313228681746121310495054414996059656767348799556081131195168)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_263 :
Polynomial.coeff recurrence4Scalar2Second 263 = (((760541080613346795191862605 * 10 ^ 70 + 7073429239835332227029676111428896265937878461284745720102601805160854) * 10 ^ 70 + 5064948404481842852701377312079954445760755269040111284140153431225482) * 10 ^ 70 + 7541627467130310372044042423083706445420028792947055961173639782222759) * 10 ^ 70 + 1623620710539232993340866235804380598635916846942042058055370650365752
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_264 :
Polynomial.coeff recurrence4Scalar2Second 264 = -((((597472708247776478353057170 * 10 ^ 70 + 7654606943071238109635447495723828278683869270036862203157651109481692) * 10 ^ 70 + 4915309443732969561412882887104621708126021666848380631898091255921350) * 10 ^ 70 + 3930823940717148639119679022880084920326448543307309927894325161229239) * 10 ^ 70 + 443619590841716388450008328124257934515363927283461495352978822695150)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_265 :
Polynomial.coeff recurrence4Scalar2Second 265 = (((447550473670227238263660913 * 10 ^ 70 + 7780431212478658245356504310017083170492306760205949069383115848972421) * 10 ^ 70 + 5322746373816541425658184368666720034286352770501614074929898674430252) * 10 ^ 70 + 6746216143579392693443181853331986938756086109425100481100753481945018) * 10 ^ 70 + 2650323534001144217278730626601607472062670422756416977930141363038582
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_266 :
Polynomial.coeff recurrence4Scalar2Second 266 = -((((314784313456937445212466038 * 10 ^ 70 + 7681293856997151689519273813884324480149818884689527872639499002612240) * 10 ^ 70 + 1205044391787234414775609156342038207000891410594998386530094076603558) * 10 ^ 70 + 6742962029289420881700346797532669135779235741009712225447781008506301) * 10 ^ 70 + 1972271912667198338826675615692936903452050546777684440873975810837701)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_267 :
Polynomial.coeff recurrence4Scalar2Second 267 = (((201640783580780987586926897 * 10 ^ 70 + 120996859328443127320285264792328154462379511548541949456680179133505) * 10 ^ 70 + 3130050798057809649183391608149990382613093996444391383025408673669052) * 10 ^ 70 + 9779113552762253485910618748368999675150418600813183666307826601674154) * 10 ^ 70 + 1391508427332640129504412556081172887770673668206199265145124474082397
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_268 :
Polynomial.coeff recurrence4Scalar2Second 268 = -((((109105010876330802145974578 * 10 ^ 70 + 9561674527559812469549161949852226482495589139192044405201138789675473) * 10 ^ 70 + 1160005021641124159451239359873643122758028588012572339545313293806555) * 10 ^ 70 + 8493176533658290172006124935281755916213852543091827907235705242512999) * 10 ^ 70 + 6395613610941479459256240514932559959057740588361347845625006990603410)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_269 :
Polynomial.coeff recurrence4Scalar2Second 269 = (((36854349200274361248162063 * 10 ^ 70 + 7227830894178320360812159387083181011940909508055264856877606345145320) * 10 ^ 70 + 4517831650825608053272571200794170296861233469782453239555644442674622) * 10 ^ 70 + 527689977388736037242807361277313811571475454519189820872997532390285) * 10 ^ 70 + 2777917621136458887437580987975058007731805589801370390629017590745305
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_270 :
Polynomial.coeff recurrence4Scalar2Second 270 = (((16489870340346019429828284 * 10 ^ 70 + 313955444727064457094154618668115033563658230428358889037881538466634) * 10 ^ 70 + 2284861954228682924587672131266253987129696126206108802692144718784313) * 10 ^ 70 + 8329561087193839788230664077492446147712569292182105380982074928867497) * 10 ^ 70 + 9422732453299936768210665316528239119347402297432202118338970238277330