Recurrence 4 lookup certificate: Scalar2Exceptional 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.recurrence4Scalar2Exceptional_coeff_342 : Polynomial.coeff recurrence4Scalar2Exceptional 342 = (((4550570848 * 10 ^ 70 + 8305710022749220209904118579368991346198650144706145869262756125742232) * 10 ^ 70 + 3051395307276017502704552818829219219950222204702678245103615431392059) * 10 ^ 70 + 3491374289896050439673451432006712699168076384268398420342241316431403) * 10 ^ 70 + 4030992659551597130118935544402388293668876197649549528325795700807926

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_343 : Polynomial.coeff recurrence4Scalar2Exceptional 343 = -((((2041676602 * 10 ^ 70 + 355481268032800414456839116017360598807845850333717326296519136701029) * 10 ^ 70 + 3603670067673465396322424766505627524984344818917278578360680725615108) * 10 ^ 70 + 4422942077400592610282376998598526793636750849888104522124979203592192) * 10 ^ 70 + 3396423144277636185561815461069876320148171195281465788979294972909415)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_344 : Polynomial.coeff recurrence4Scalar2Exceptional 344 = (((905552560 * 10 ^ 70 + 1503531462821730953432545768234426317307043407157551519271457139872090) * 10 ^ 70 + 4008586709507604053176936357774303774624281209339864123386427935440450) * 10 ^ 70 + 9012842265305368523878839428208360360663921150229428815166742548804702) * 10 ^ 70 + 37779544512615947023427577693677181336932474934882006641452937216357

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_345 : Polynomial.coeff recurrence4Scalar2Exceptional 345 = -((((396673383 * 10 ^ 70 + 5679809881646417925547569464603265124104902782698994199853457979361817) * 10 ^ 70 + 149678118879948858930009105520999611967481953220207360695046447356538) * 10 ^ 70 + 424836633192366251699740654405246175218482717668052517870244450654509) * 10 ^ 70 + 3622303185572608136530742378141180533963301235189084444531648998168073)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_346 : Polynomial.coeff recurrence4Scalar2Exceptional 346 = (((171476669 * 10 ^ 70 + 3779304097619054629806752982584330672632625654405358131874559851661062) * 10 ^ 70 + 7605309470357935347757251831625265498655938533781199904703255213762307) * 10 ^ 70 + 4557982245990194925596470320855448954943388797923628615324403452438261) * 10 ^ 70 + 5474613887646384534882457999699704519947621366068962497070140605713243

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_347 : Polynomial.coeff recurrence4Scalar2Exceptional 347 = -((((73103267 * 10 ^ 70 + 4861021849604298967511245540163703862355275897476184189671953375125718) * 10 ^ 70 + 2114545409157916072695313409105513958052736339809217212488633830666754) * 10 ^ 70 + 6707914307820486825893364009456478990714774693165388721289690558428865) * 10 ^ 70 + 5765249201194178323229064240306087110156844816096559536176409109794068)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_348 : Polynomial.coeff recurrence4Scalar2Exceptional 348 = (((30715037 * 10 ^ 70 + 2503366201580755286344280396796728471917063512722135866383429470438128) * 10 ^ 70 + 6204387210654887195542485721516757563408401862178269604849786689221054) * 10 ^ 70 + 254377523744286017514146078176516337786556939485827684725340624468825) * 10 ^ 70 + 866834175766191720959673945781840805849269578330639390635754609260589

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_349 : Polynomial.coeff recurrence4Scalar2Exceptional 349 = -((((12710037 * 10 ^ 70 + 7443563025464858911498268086851215021726652733441654012131041753348637) * 10 ^ 70 + 3190848570462724614892882250462638549068349005042791849937605257221672) * 10 ^ 70 + 4921564629461995130265904302033404824870818890591528277954229184133946) * 10 ^ 70 + 4871242654505667327500129062816985597636757920135039344430631559498431)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_350 : Polynomial.coeff recurrence4Scalar2Exceptional 350 = (((5175466 * 10 ^ 70 + 2616015235490844682281303132815376552602059826341638056914206195065309) * 10 ^ 70 + 1214531236316644231313260522211770724203109593539571031916222777196221) * 10 ^ 70 + 2586868837956194538346678104382025737153972290727140500231027875021871) * 10 ^ 70 + 1517409320058782444041497272295547688503467773757141706190437612380481

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_351 : Polynomial.coeff recurrence4Scalar2Exceptional 351 = -((((2071304 * 10 ^ 70 + 17955371401068111757937667921902958878389033189141682256607976724539) * 10 ^ 70 + 1848691465583185492567140130934899395921721769967218002601411751289259) * 10 ^ 70 + 5569065939616996616289909618040388359236560279732019625305289349680303) * 10 ^ 70 + 6961484018127311748721327890703384084180998719937569771498705294174989)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_352 : Polynomial.coeff recurrence4Scalar2Exceptional 352 = (((813355 * 10 ^ 70 + 1200248009674869553433885294844494411980460596970677855047914018095386) * 10 ^ 70 + 6341917058351013482344655513191161943338155723963876407249265301802889) * 10 ^ 70 + 7507976691127837355138597183758436212317702937913299184692627933669221) * 10 ^ 70 + 32960743190049753941348462479355452952352041187446871183803156178490

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_353 : Polynomial.coeff recurrence4Scalar2Exceptional 353 = -((((312559 * 10 ^ 70 + 1841535139445071589012536724959050378814354490137760336303843791984491) * 10 ^ 70 + 5351875134308496003521139426010223553067026394243325898575075938711592) * 10 ^ 70 + 467234861846634324180941098846051614531615442654906570876154244170391) * 10 ^ 70 + 4896066397761932889698166641581896369861677201030649053943771194931307)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_354 : Polynomial.coeff recurrence4Scalar2Exceptional 354 = (((117075 * 10 ^ 70 + 3556320130244983298005941560269989352775209689781803952176316586794196) * 10 ^ 70 + 81725799177874567027966204617227797585627031839860560801229752669256) * 10 ^ 70 + 9073222295231637457337752196493013736077122118242299282550822392417600) * 10 ^ 70 + 3658612429758281812340243004512617368643613409182261405404544146391269

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_355 : Polynomial.coeff recurrence4Scalar2Exceptional 355 = -((((42473 * 10 ^ 70 + 8646358615904177271482016330693970879218899372941785216930663403491164) * 10 ^ 70 + 8509797035068171868376045524349308314714145458066741586702677862713476) * 10 ^ 70 + 583634687810777870294890558711822903532898647790025521773945893214563) * 10 ^ 70 + 4991924632682831536907842870316738720729390938220854553595548842897655)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_356 : Polynomial.coeff recurrence4Scalar2Exceptional 356 = (((14766 * 10 ^ 70 + 7635805122269300012229792197228236272283358206258118144468382716560030) * 10 ^ 70 + 1532188718881105817552278432441537223312477598099994677608486209621621) * 10 ^ 70 + 7202093018570352812975686963966806867809489138282157495724031943800815) * 10 ^ 70 + 9875382349767414665820322161453471308774261618764474496312457636753251

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_357 : Polynomial.coeff recurrence4Scalar2Exceptional 357 = -((((4825 * 10 ^ 70 + 5534263038107987120806390144552719864703882786239915554586178269842683) * 10 ^ 70 + 4742341886164576172440960703820043298165733100984775802184849845307938) * 10 ^ 70 + 20933395574541972676918261940933296378138213318568875164759518566868) * 10 ^ 70 + 5182693922123186694429877164406792923164598084701508191900713319001677)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_358 : Polynomial.coeff recurrence4Scalar2Exceptional 358 = (((1422 * 10 ^ 70 + 9937688978257451180182805323054101552270689848159297710477116179752348) * 10 ^ 70 + 420231275019453203031300757953056620778385771197840728211315901957066) * 10 ^ 70 + 9394724925823725869991344130331053996501037626928124373900889307665751) * 10 ^ 70 + 759415388946623400757769410497726332706789024424222377975494644747917

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_359 : Polynomial.coeff recurrence4Scalar2Exceptional 359 = -((((338 * 10 ^ 70 + 2600988871296492248371894021186199559707625066512113488270717826061912) * 10 ^ 70 + 6442619108311795732173243853918598381921390188013394422028273653001341) * 10 ^ 70 + 334058865371292333081232403329873233012105646614652975531099921848617) * 10 ^ 70 + 7993091307900768869705586105427979156564659281580627882310208864118598)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_360 : Polynomial.coeff recurrence4Scalar2Exceptional 360 = (((32 * 10 ^ 70 + 9661615092047706977116331461847810171830263103897241183420210740000487) * 10 ^ 70 + 718570625603354394455131953639037133568488940430078386328066524076931) * 10 ^ 70 + 4150444881148406657567418157908360213911710111865890971499284571731861) * 10 ^ 70 + 6920154246249907847818108495537853384003063448982520104495060087153243

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_361 : Polynomial.coeff recurrence4Scalar2Exceptional 361 = (((30 * 10 ^ 70 + 9960113022549560304158749273636076946093912480076613474068197712330726) * 10 ^ 70 + 2944979948644239936605559413920253898315673270088904712948387126521638) * 10 ^ 70 + 7286411825625170873805670897110325171187409315690970447057839303718785) * 10 ^ 70 + 6946912924978514385459906153360055322366915917559353900111673728817935

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_362 : Polynomial.coeff recurrence4Scalar2Exceptional 362 = -((((30 * 10 ^ 70 + 9748474361352242166734734333550860351991632140521438351984879613734996) * 10 ^ 70 + 4755669950164290060757447056223880105290844431858599249653997248748232) * 10 ^ 70 + 3040139645167116692275735279886107187984708073431246795510165189847028) * 10 ^ 70 + 2136825533296835843131892638836602461022291092276220001013658805713703)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_363 : Polynomial.coeff recurrence4Scalar2Exceptional 363 = (((19 * 10 ^ 70 + 9848691680277069223102433497876794298941888608774363058530420441444411) * 10 ^ 70 + 4118149566575311738764362093395883897363416282141969897499522388791096) * 10 ^ 70 + 1432966540038766073424523493375721756546904458709018653598915335110975) * 10 ^ 70 + 383186064020304245151003164310280015286820439513665527523073142006559

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_364 : Polynomial.coeff recurrence4Scalar2Exceptional 364 = -((((11 * 10 ^ 70 + 56492858908783541365054433184178258247968168152647193781137376565828) * 10 ^ 70 + 8162686105589829523834453796048041474652936529851363998929717210648624) * 10 ^ 70 + 5650094914664658661185285353051161511578804835328998656398316342656536) * 10 ^ 70 + 5662433746895533167583307008572971476177106550776241530820007826297770)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_365 : Polynomial.coeff recurrence4Scalar2Exceptional 365 = (((5 * 10 ^ 70 + 5560308019321073269542192158478870727020922839316668121253305776162806) * 10 ^ 70 + 6180200613930040915722509104849829921273979885243132579487982260530820) * 10 ^ 70 + 3582228730538067473989762334935364594356586112291148135040373602067339) * 10 ^ 70 + 8113525395704629340978169849416764423479923909182343715854229828187740

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_366 : Polynomial.coeff recurrence4Scalar2Exceptional 366 = -((((2 * 10 ^ 70 + 6468920060127490325608888437456524072276022219505317997384661066625273) * 10 ^ 70 + 5664449472259634473186329337363494168205446963970470847495709340417373) * 10 ^ 70 + 3413676323028267144968508489966945726553414179061806556990484844894850) * 10 ^ 70 + 5775072772567751626569413743434477784382604151598226357751920123594934)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_367 : Polynomial.coeff recurrence4Scalar2Exceptional 367 = (((1 * 10 ^ 70 + 2073130628377063361187135447029293486825277324591570143970803795391400) * 10 ^ 70 + 9842038360263658892878917485662319055316912237702361593534838081491319) * 10 ^ 70 + 5568707208703325817559218248663864489309039055219007869813708821822173) * 10 ^ 70 + 1509483552712512722492163631045631987595561788670637595916168220076254

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_368 : Polynomial.coeff recurrence4Scalar2Exceptional 368 = -(((5315662531450233381575459720058099652785679308909897335174340696321066 * 10 ^ 70 + 7691980299934941194523997861048298771015763157572953723240414027234000) * 10 ^ 70 + 8635026097954207778590603876451661494951664784389379919291111321100536) * 10 ^ 70 + 4043444040203757169549081313867746132700195223874357303660019031100864)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_369 : Polynomial.coeff recurrence4Scalar2Exceptional 369 = ((2270368298018531185156725721770368752689186844468808978969468905387598 * 10 ^ 70 + 9766309484203196084240670558953610100008542668723725274538171996296891) * 10 ^ 70 + 4653532963307194614862334298794648319856268934111517988282444297378666) * 10 ^ 70 + 8491430164146369937496324212776401878484347465777646585448541746891623

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_370 : Polynomial.coeff recurrence4Scalar2Exceptional 370 = -(((943610668473053246285886005985093815972363690134690727478412300968528 * 10 ^ 70 + 813839634055231599630929723913914889642551053741100958288387973235857) * 10 ^ 70 + 8521395952647569280259670094054568686565038723182940526103071817142184) * 10 ^ 70 + 7220676946790523062604603587917095540524277494435700794379994624587826)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Exceptional_coeff_371 : Polynomial.coeff recurrence4Scalar2Exceptional 371 = ((382387899632330942034047004120954299401221768507386439296643093075782 * 10 ^ 70 + 315911581833393661460579268041021913063663349318372018260700632619689) * 10 ^ 70 + 6581061522782876677995785009635508978764921115250583522109189231276668) * 10 ^ 70 + 8162854526517040578264825616452500420459428151680891607259195042823386