Recurrence 5 lookup certificate: Scalar0Main 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.recurrence5Scalar0Main_coeff_338 :
Polynomial.coeff recurrence5Scalar0Main 338 = -((((6646357345391990589873980274999034270275942817721674 * 10 ^ 70 + 8206552704166840089172179052466680567841862808936275469362818660061539) * 10 ^ 70 + 5449318942182964694145910849767182896210363827674753963617176125835132) * 10 ^ 70 + 1295708000405656406642431125121267720870924498335333968610711338501465) * 10 ^ 70 + 5409496030908431523924005472709228983523852050620381097759676886446154)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_339 :
Polynomial.coeff recurrence5Scalar0Main 339 = (((2683013380076624365589390630382915085175777860574192 * 10 ^ 70 + 5311887831277130821034085640336663527954412666419526031012658740949778) * 10 ^ 70 + 9519342747150664148683741412874819369347581947040861405951938768622514) * 10 ^ 70 + 3439070870045670106812098519975140401874503933934866058748491729305426) * 10 ^ 70 + 4140436586945502607102837367340592275633310657793613035946715993187988
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_340 :
Polynomial.coeff recurrence5Scalar0Main 340 = -((((1062711968951584695708929105054550428615221388143248 * 10 ^ 70 + 3159167105032165531248517800472964386025295315492503827121035107592690) * 10 ^ 70 + 3564651494302620467206653715849979071489083859594692717050376804992342) * 10 ^ 70 + 8582625551029102708319690827129583849126523453926592513328064250712184) * 10 ^ 70 + 8680487875019425458320380620090171263302235868530888161406273670447404)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_341 :
Polynomial.coeff recurrence5Scalar0Main 341 = (((412614423602051147332769585116830194933310297003152 * 10 ^ 70 + 7027576619837143324751097814215094352940309553195608177194191883688308) * 10 ^ 70 + 3901458489216989482043798679759224215260775806664413838512161314616541) * 10 ^ 70 + 1765867390105823159330281927028139863739567168390905267216541188325166) * 10 ^ 70 + 3274891902216062892143282737870304071331569098018983270382945719757224
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_342 :
Polynomial.coeff recurrence5Scalar0Main 342 = -((((156893598880308479146161843550886527954486325079394 * 10 ^ 70 + 7540148030758026237456251321519120761686027282542259270505864823882649) * 10 ^ 70 + 4586283771698366000697235413542726981935735433985267655978366854259117) * 10 ^ 70 + 174058310701873179109067048082680126259928054952449466215752576494867) * 10 ^ 70 + 8147453832263612487009603878071830735008708642382009439453239584890892)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_343 :
Polynomial.coeff recurrence5Scalar0Main 343 = (((58372351227104008884886475990617311145099943910678 * 10 ^ 70 + 3775670328312124147006468825137356486808451961986596433646026084798947) * 10 ^ 70 + 4576939653390862384925275857866862797007679204966536371495712283219020) * 10 ^ 70 + 5873869483534466255343263947440749734146647161466649669044446331060214) * 10 ^ 70 + 6586770590761164986502330456903060245198068536432951144777540405651937
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_344 :
Polynomial.coeff recurrence5Scalar0Main 344 = -((((21230677262887106905479756858647388834658369646683 * 10 ^ 70 + 243661061775176010288841598063915229280703989238375935020490683460912) * 10 ^ 70 + 8983769880502432682921488507881084756202147000704291578788538774832612) * 10 ^ 70 + 5494059009814436437969256627555874135269540005186308583282049275527353) * 10 ^ 70 + 4291959379962129929939970834006649078103082109794699496160239256995111)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_345 :
Polynomial.coeff recurrence5Scalar0Main 345 = (((7541807321178365365552515665946004264542122140401 * 10 ^ 70 + 3767422017245795064243151106182905344725070791766978343340012200473850) * 10 ^ 70 + 1896792635638540515923728402913662337382297121864148174563659534393328) * 10 ^ 70 + 5376589518640663630883087632855896582785525604700509696621147895158073) * 10 ^ 70 + 7559732202506880530612087286755075925111214046119664638969379551345398
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_346 :
Polynomial.coeff recurrence5Scalar0Main 346 = -((((2613968617029313797429993472780248232207423295706 * 10 ^ 70 + 2348823473497993947865069047562269077263530781414300859475455739834814) * 10 ^ 70 + 8809961827692486204749082262538030815704780963500266046582902278358290) * 10 ^ 70 + 6541893722139710353671760015691952868239447085337946923791726978900332) * 10 ^ 70 + 1129238511750199063804642970268372332945957667297923004792553932852928)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_347 :
Polynomial.coeff recurrence5Scalar0Main 347 = (((882900013131906372030113835408277389698106501619 * 10 ^ 70 + 7881287970146205121758166108920389585064735822528056396741997210596653) * 10 ^ 70 + 9416730190804445513444354400175620144606318677692395220012865810146456) * 10 ^ 70 + 5939124319053969597483022201346519085484978320458309819075619296252319) * 10 ^ 70 + 7645421336404721700643872454687579424335777685982865555203306198916195
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_348 :
Polynomial.coeff recurrence5Scalar0Main 348 = -((((290153530169998064731747449877791111073942102817 * 10 ^ 70 + 9717014674366660890304181840010068343294326611919262478440005187151738) * 10 ^ 70 + 3873634491769555637709919201854205361666097070229668403721871019517848) * 10 ^ 70 + 9405070151869146957955313510546138509026202984212941127833838054381541) * 10 ^ 70 + 9373668628761999958159490754354629715649184661732844183523925163423435)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_349 :
Polynomial.coeff recurrence5Scalar0Main 349 = (((92577052133871547668790349602065173814220948371 * 10 ^ 70 + 2997078516662588993182929085364042226543377395775479038657279143561721) * 10 ^ 70 + 7252967805019256406729805014890645901311801643679600027434065445036813) * 10 ^ 70 + 9161315233084397112423937703659936498163912308417666136030448193765577) * 10 ^ 70 + 7712969448409425094505518731545662805416700720819480512394411508856224
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_350 :
Polynomial.coeff recurrence5Scalar0Main 350 = -((((28584861005342224097261074285594851541693611666 * 10 ^ 70 + 8542784118859072268580506206160718117036911742972625902596254986030379) * 10 ^ 70 + 517120771686307260028654710926515527476483224720615642347151738943060) * 10 ^ 70 + 6359878786793024953839939668648099693618693201180312627289172880888848) * 10 ^ 70 + 2149906164620786066318667522025403408350208564083562287721829358814403)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_351 :
Polynomial.coeff recurrence5Scalar0Main 351 = (((8497995653686911286880609445215429096817931015 * 10 ^ 70 + 87607117800142041002867462812588104131526290392331536122442971308212) * 10 ^ 70 + 7949670689102781687562599935288814332750082052627872519422685632261815) * 10 ^ 70 + 1188938318102690464588425656535529872795338585648113713967196281851442) * 10 ^ 70 + 5420218728300856248128389178050872895021949954965875051573744332848952
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_352 :
Polynomial.coeff recurrence5Scalar0Main 352 = -((((2411671151680648316712715883645330650528471209 * 10 ^ 70 + 6419807883745864910951149715983738575392431218829733225883724657700925) * 10 ^ 70 + 5086599066983374037298935369915258869354023674971192805043234504833908) * 10 ^ 70 + 4907067320491816109259530273621940920328398743054723214887038528006685) * 10 ^ 70 + 8896500805853605807024735483592098516542690675298275512229234851979394)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_353 :
Polynomial.coeff recurrence5Scalar0Main 353 = (((643104981430192337720450924061267886952096764 * 10 ^ 70 + 7214043412023067951394621140190366444294233389788836483974248799512283) * 10 ^ 70 + 5482144124768874365324904885795733646870781538218251108104675862077529) * 10 ^ 70 + 1073557300099449767724776880072697381447904141241800699788463052629288) * 10 ^ 70 + 1664174958404519067951853126055303742311401453157847489887239082949773
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_354 :
Polynomial.coeff recurrence5Scalar0Main 354 = -((((155889296192914221670387699287256197642352541 * 10 ^ 70 + 347281105497207367690554491079222572483945158810739674124078234488819) * 10 ^ 70 + 2375477019356485275475893129794532322912293746282111038431515892684827) * 10 ^ 70 + 9515436932686770345348971367992523553528859467888639670842818982692898) * 10 ^ 70 + 1039387229191554757763027786567978414067784916562143264895741650434891)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_355 :
Polynomial.coeff recurrence5Scalar0Main 355 = (((31466082230723548792126647010414872970415677 * 10 ^ 70 + 6658468964691010408138434471508206632960000115736379102709400485780395) * 10 ^ 70 + 3665343552025719145262449006588293014606750556652488031715217662718870) * 10 ^ 70 + 8726230084211166913000656465964198102961747915005481609041605824308874) * 10 ^ 70 + 7070457771727406643212191081208632400688081875606280041947758051930497
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_356 :
Polynomial.coeff recurrence5Scalar0Main 356 = -((((3504658466625329799962385636280659610350655 * 10 ^ 70 + 2893556412664629592505110634208218985549789307333880586149531669145491) * 10 ^ 70 + 7498843613602489016277709982569693877557709852365584269593706802592900) * 10 ^ 70 + 491832414839233224126002292956149446196918552017085776979213309535511) * 10 ^ 70 + 2629029010024061013444558604944886839149712032417732185991806179424671)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_357 :
Polynomial.coeff recurrence5Scalar0Main 357 = -((((1161687644433421417556988157405784685736816 * 10 ^ 70 + 7460314231176602246798653502760713394906021771877468817183137020256337) * 10 ^ 70 + 4188161347512674112559610469008694929507132544240233241689008356886650) * 10 ^ 70 + 9443693328864391815500391599939605174769216439250922473400735772182025) * 10 ^ 70 + 411343622994416723338190774278182514328741321863611234235605731332752)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_358 :
Polynomial.coeff recurrence5Scalar0Main 358 = (((1152860365448186011844101538180976396125895 * 10 ^ 70 + 6295227307324304911954750905998186070871703497263532798353410069823402) * 10 ^ 70 + 9946555883975417695107126015400802144722208413007575192567658659637527) * 10 ^ 70 + 7283600538083587949957234818221754775359412667384509373498809677424674) * 10 ^ 70 + 12634130195725558871866437190305468957488293584767994895700032401462
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_359 :
Polynomial.coeff recurrence5Scalar0Main 359 = -((((633346122229111887427306086903589046895582 * 10 ^ 70 + 9773683112093155188963359638500936959627363511925919054297496462291667) * 10 ^ 70 + 2258837758629532904859586823115358692663910835791551555780848418406704) * 10 ^ 70 + 7850718549597907612395487647431051773205625263712690953724001434801633) * 10 ^ 70 + 2809195712845565105931048785466214136540077822965980890771993582443498)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_360 :
Polynomial.coeff recurrence5Scalar0Main 360 = (((291591997527274660733073155593569535067494 * 10 ^ 70 + 9280876470524607996693817677210912879992611035850157368620597413731168) * 10 ^ 70 + 9005209868933650328886007154923800164480418077018621723374802731976504) * 10 ^ 70 + 9272028360549822116770601829968504273775445117964824500720969302371877) * 10 ^ 70 + 4881210676224664743031006849078124170682166200100638878860590892109375
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_361 :
Polynomial.coeff recurrence5Scalar0Main 361 = -((((123058870246476339003122077118940589701292 * 10 ^ 70 + 6710642952241946738160239882093003524090891369260876617921213576818941) * 10 ^ 70 + 5362000803018241198031405212594746400590289311062126867139750495561064) * 10 ^ 70 + 3149757336934527788597089456584553351757878111516309510553469702556127) * 10 ^ 70 + 3467806611926069605297870903530447623726733243449284921697847741936379)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_362 :
Polynomial.coeff recurrence5Scalar0Main 362 = (((49272167326149971273234548828355645898603 * 10 ^ 70 + 3466972568350037756719181225939422381830489025971740856340925632329742) * 10 ^ 70 + 8168919330295318781943074783433125040316858081310229072403456550386704) * 10 ^ 70 + 5540092553194064937862755178144191687377242473013430998550073235641576) * 10 ^ 70 + 2591606438175671916973218684402330564238494413739094430559294601812989
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_363 :
Polynomial.coeff recurrence5Scalar0Main 363 = -((((19026785410374987774805671900645965871412 * 10 ^ 70 + 853058229733565807898689788659862816294435433781247856505566479075354) * 10 ^ 70 + 3432280628858943556983487198884008345161589061607901474499196136074129) * 10 ^ 70 + 9118616641760656160970309113207754075145948724668070230428079720222277) * 10 ^ 70 + 4821758499748885089216526516888252814220501915273128247317884401621639)