Recurrence 5 lookup certificate: Scalar0Exceptional 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.recurrence5Scalar0Exceptional_coeff_362 :
Polynomial.coeff recurrence5Scalar0Exceptional 362 = (((29435116235383485643576584559783213294 * 10 ^ 70 + 7480776512814967545508399224625389051902536798126603268977840176676870) * 10 ^ 70 + 1330007441146709897478473792138285457366735466434922782122700889416959) * 10 ^ 70 + 7746132473737738903383706792360804075945435243784803377801818970745948) * 10 ^ 70 + 9925481255381758636873272411761322039834673649251300624743488566954579
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_363 :
Polynomial.coeff recurrence5Scalar0Exceptional 363 = (((230544999427900837796670210252842949650 * 10 ^ 70 + 6510194054173244544195726608438597311097906231808213280916107522508892) * 10 ^ 70 + 2240278030685340083834649045398278564625377562465780803773952289871291) * 10 ^ 70 + 829021351837148945011073227759166444735806887455053980606013380951921) * 10 ^ 70 + 1769007776238892933281273146559230113731406367734479485146590531934602
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_364 :
Polynomial.coeff recurrence5Scalar0Exceptional 364 = -((((147204207766264857430637660396011262893 * 10 ^ 70 + 4842428774714491092265181919234577503958828057588365235921665210308837) * 10 ^ 70 + 5638665970856630125347058674458673450704251059062161173169830461236771) * 10 ^ 70 + 6013192755949987592494473890028027803235429717819915686158539268203382) * 10 ^ 70 + 3761562400281370068964097290236851482156735967474582456198448460221711)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_365 :
Polynomial.coeff recurrence5Scalar0Exceptional 365 = (((67523499025016574210911733795238724341 * 10 ^ 70 + 9408467215869091669208882652678813175368975268186011133807915528153578) * 10 ^ 70 + 1837254260791131239261844414021133773506787573855067873407613048706273) * 10 ^ 70 + 1378824269501147413773725250523992799372471500733344198776440952029477) * 10 ^ 70 + 5152740517540266316088366582697313122126720824781861102998145719186866
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_366 :
Polynomial.coeff recurrence5Scalar0Exceptional 366 = -((((26672762425658689260559784422586516222 * 10 ^ 70 + 5838853247578691995809566803740801997538090187734957552625336535870218) * 10 ^ 70 + 9660677329524746494175057441508113186578559833832439951366270434610495) * 10 ^ 70 + 360647563274143929858719462463039796173388230134198416558933011609503) * 10 ^ 70 + 7555248534707541115642156024099955215305495752808048208495299407123949)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_367 :
Polynomial.coeff recurrence5Scalar0Exceptional 367 = (((9595170259841593304962793195665539570 * 10 ^ 70 + 1306411296491244387257025975527972623785901419909929844298064504571656) * 10 ^ 70 + 9904583984925863069513573819598686411031345251043409390175613306115433) * 10 ^ 70 + 226924864501653685034481564717392511466156174769371924797812818885576) * 10 ^ 70 + 4181642385252948038202381764015237304787426763523387047354309655161957
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_368 :
Polynomial.coeff recurrence5Scalar0Exceptional 368 = -((((3220026989510210781337270039812384757 * 10 ^ 70 + 7739772329814458321795932713812463436940394537948732089608418012195669) * 10 ^ 70 + 7159428490507344993199400629314942866467615643972423651446178621103738) * 10 ^ 70 + 9118530382179672360081354135580795005209340979763931353159834863193376) * 10 ^ 70 + 8282682667543111683670776114567293004749518705990324440323790809967395)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_369 :
Polynomial.coeff recurrence5Scalar0Exceptional 369 = (((1018736858636595180858051455269715758 * 10 ^ 70 + 8598487109093052213000453506306374889459445646248247340909168861185327) * 10 ^ 70 + 813195536673366965270923690465274494539243376292691423030301984236351) * 10 ^ 70 + 5050320434871848499733267571636258589394933527419961283031046584821142) * 10 ^ 70 + 4618789061412235334885924753883657347638991595579926622266994261297142
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_370 :
Polynomial.coeff recurrence5Scalar0Exceptional 370 = -((((304261830944006150323033164881006578 * 10 ^ 70 + 3026271810163068497407730783068095471087687854356117036942215215847135) * 10 ^ 70 + 4765565775726013195356858542850611513720869701863760254129971778253492) * 10 ^ 70 + 1394720168293790839030803654539682217284366504525575554314226589240651) * 10 ^ 70 + 511765761107076672920932849206071436554477983684755141045614952775346)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_371 :
Polynomial.coeff recurrence5Scalar0Exceptional 371 = (((85032183177046526251924220752063365 * 10 ^ 70 + 2035059336269639827191851999285495794380501564051095609505968071260683) * 10 ^ 70 + 1751002016200294600304979276163442850344593597377979509199761262682734) * 10 ^ 70 + 7259925812252699883713382692496323559215383149649727673541654526327939) * 10 ^ 70 + 4722395280872996265092503706730607199396018283528396512573437218096929
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_372 :
Polynomial.coeff recurrence5Scalar0Exceptional 372 = -((((21662477599760598223180497525966910 * 10 ^ 70 + 3609707277979837562585004566092391006931471335930570329423754253230957) * 10 ^ 70 + 2039886252527123147591498085253916722227582291743713436809306065025017) * 10 ^ 70 + 450046985030109049081728449551533546425179916699646624545358953368315) * 10 ^ 70 + 1054542899024917252985884471339856550617925627162054289203984359347774)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_373 :
Polynomial.coeff recurrence5Scalar0Exceptional 373 = (((4687747999504633125682281632226211 * 10 ^ 70 + 6840672591405040769798541584720656844465472317122469474981939330432838) * 10 ^ 70 + 6749745446005726795252679483925529532719499223014402189420627522685604) * 10 ^ 70 + 6677032040412663459879506827556174235108803145834181086188235565676224) * 10 ^ 70 + 8246146257167614795942084530227195684444034348922240319756195813795889
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_374 :
Polynomial.coeff recurrence5Scalar0Exceptional 374 = -((((652315460367372049590862177992190 * 10 ^ 70 + 8251256325873004243161420080673400592814307370948551549274794758000061) * 10 ^ 70 + 2895818527708670031968424719566622317403579864925412382167265631702458) * 10 ^ 70 + 2111029224472498663514853045961274141652576713708595198795956484383300) * 10 ^ 70 + 2973332251550589884557034628898358706740567358481385504194459093035235)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_375 :
Polynomial.coeff recurrence5Scalar0Exceptional 375 = -((((93802550869644877153174871730824 * 10 ^ 70 + 4411677630706956525034044976204030125773172098803800047703330009000139) * 10 ^ 70 + 6857979310909813792709569736580943970450366797933336277838939517227393) * 10 ^ 70 + 1293288778177337034869654287249504307714982396890358888412259207747134) * 10 ^ 70 + 7878159973653456354697076761417044096001030326318014697657436135766656)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_376 :
Polynomial.coeff recurrence5Scalar0Exceptional 376 = (((132069877565798136906606980398866 * 10 ^ 70 + 9426967394931623540695851186621321219817073233469202768587482571603755) * 10 ^ 70 + 7400550309337486638545196042941421813925529090109357368728163872327006) * 10 ^ 70 + 8655957457994951356058344603073582829646014894199105880248897646417720) * 10 ^ 70 + 4536445133466809736369600416716640271673455416987901425115998121127238
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_377 :
Polynomial.coeff recurrence5Scalar0Exceptional 377 = -((((74590397132807205247050435219055 * 10 ^ 70 + 9473593636318913509291794030090039871943502581723403982870745103478250) * 10 ^ 70 + 9492658478452233602224985885151397081041022543157886319159864277148603) * 10 ^ 70 + 8288921608773664284655506905773544950482107312857247587290697839219720) * 10 ^ 70 + 5591269381258091288938224616315264181064598469031769643277702970727692)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_378 :
Polynomial.coeff recurrence5Scalar0Exceptional 378 = (((33348297839078275692822459238432 * 10 ^ 70 + 7963734300042268940361470680813574117466761654083157050757215922699607) * 10 ^ 70 + 7334003599511597363752718197613331441761337162251465734858418429673310) * 10 ^ 70 + 8074253279035798517551617369639673685880803957895222342269902061026846) * 10 ^ 70 + 9379709858183660041460662676329827804722714380001923656830286089781059
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_379 :
Polynomial.coeff recurrence5Scalar0Exceptional 379 = -((((13169158377498703682131436313743 * 10 ^ 70 + 5268638314800270182545513984117022842091393761898873811001238250836051) * 10 ^ 70 + 3998447139785200949032076201345112013259126792701897173178562950781686) * 10 ^ 70 + 7019492699706551114132301935361717090321089225751072176650649119544098) * 10 ^ 70 + 2184529165340450118044688077569202702958953996901332772290713753158430)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_380 :
Polynomial.coeff recurrence5Scalar0Exceptional 380 = (((4764600176481747876416243417584 * 10 ^ 70 + 1563138393846190167270557638859209016542224693253883396213720451021661) * 10 ^ 70 + 395041327176849005860435057920340989603982472324531418399219247621617) * 10 ^ 70 + 8715583865637690970278808126464400125843337500230420290769834236536448) * 10 ^ 70 + 2592776281488552345101098290574915501643381442600667890305229611941720
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_381 :
Polynomial.coeff recurrence5Scalar0Exceptional 381 = -((((1602142210554909815100350092927 * 10 ^ 70 + 7110935810627654301050848411290031637997986441482418508618102767086017) * 10 ^ 70 + 9243149839996026080441365336555548114528822952644210332313555634435834) * 10 ^ 70 + 7444887663560322321432064256322213424953838542173393680508778181343368) * 10 ^ 70 + 3483753536793608377373524085129006184600607487718014385936160421191486)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_382 :
Polynomial.coeff recurrence5Scalar0Exceptional 382 = (((502884225920038284793405117175 * 10 ^ 70 + 3292503288746644354325846643376635628861751326018644620825144558159438) * 10 ^ 70 + 6448929860915360983838406807285391225255913785315554056825680147370323) * 10 ^ 70 + 3246738488688475202856888920291396711724241680382510600072865844456824) * 10 ^ 70 + 6746436635183340426435570373624519187796104085886265003886109566965004
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_383 :
Polynomial.coeff recurrence5Scalar0Exceptional 383 = -((((147043811698067326139349782062 * 10 ^ 70 + 3810514685936280727180163384328640194813481650065273276491121452741488) * 10 ^ 70 + 4333333274512990429961686033433632378284405701559515772345690410269534) * 10 ^ 70 + 2968645395834178724968168643851311726645935172464437294653331231787936) * 10 ^ 70 + 7926392626452305793785438882881926162856094362519798611025030963695787)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_384 :
Polynomial.coeff recurrence5Scalar0Exceptional 384 = (((39722614000488723137422403879 * 10 ^ 70 + 5297124402268475247691473398164674000665490199231414048706503079313491) * 10 ^ 70 + 6497456406216679333988598604221279261691675890868447432019862833157282) * 10 ^ 70 + 6550091027626338471294211525504580919675127453978032476504101974127388) * 10 ^ 70 + 4957474331219357837566701695825256529069979709263547653972019133111579
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_385 :
Polynomial.coeff recurrence5Scalar0Exceptional 385 = -((((9738031536481593487408595886 * 10 ^ 70 + 6083397042099186172668776949472583633206594271743481782871636606323878) * 10 ^ 70 + 7823337506676822451195343064321186361338416660324656056216481422415346) * 10 ^ 70 + 1920918160029127062764352838055018856285252804774303366526364487406606) * 10 ^ 70 + 397486022143183512920517588493357529197919030909892574527708444579068)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_386 :
Polynomial.coeff recurrence5Scalar0Exceptional 386 = (((2083218240720392110161925835 * 10 ^ 70 + 2933339635912842845392562804748027197430798025348871428427525349718205) * 10 ^ 70 + 5267464570526660716056861808898410890498402278679511393711293904197382) * 10 ^ 70 + 4819235717700674068208136120760940362348716250710741188339804899635125) * 10 ^ 70 + 4411790115293222696206023959979331282233186356170598474136189079145823
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_387 :
Polynomial.coeff recurrence5Scalar0Exceptional 387 = -((((349005891280190077831267613 * 10 ^ 70 + 8039912816329514569519998977286796270134486233688233282998729722094707) * 10 ^ 70 + 8540059501024221521212427739558584292206471558105448011242182607188593) * 10 ^ 70 + 9167905149851523328269808885565011187167640911880187425254273933477670) * 10 ^ 70 + 8257268253399712533956151127531070373482260706909225288230070484068847)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_388 :
Polynomial.coeff recurrence5Scalar0Exceptional 388 = (((24719094239362693484655835 * 10 ^ 70 + 8130215491967299731276148547873019296733005252533128354506939097111398) * 10 ^ 70 + 5345707335855240948837928864337056429191930667686777759250527657797606) * 10 ^ 70 + 351666527598995913949077151692964398194275244336062796619521470759104) * 10 ^ 70 + 267439424127186576723507234649634584945017147929196647939042769339899
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_389 :
Polynomial.coeff recurrence5Scalar0Exceptional 389 = (((13009571709633189562178538 * 10 ^ 70 + 2882067338403296393535389135414591210716609021100904424616028202878120) * 10 ^ 70 + 2018347293071131324651326161180145734811871543238780884835077933266481) * 10 ^ 70 + 7560410506230401757451192639146734854671052672470722258792425537062413) * 10 ^ 70 + 686348558889324163263700296925520003225722488258123249810886823339682
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_390 :
Polynomial.coeff recurrence5Scalar0Exceptional 390 = -((((8387202528664712999057215 * 10 ^ 70 + 9341252891276837356134616612672614219191482509329040694061949200223906) * 10 ^ 70 + 497606554620433819813851542577272771520918453808928590680154833222625) * 10 ^ 70 + 5885577883673488870588559860444833150701387581244140082939999801561064) * 10 ^ 70 + 2376361722103181069336585556720345514619391623502569769812303968605315)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_391 :
Polynomial.coeff recurrence5Scalar0Exceptional 391 = (((3295945726678888733323231 * 10 ^ 70 + 8858598057159331958152429997519349360114425156294340751709472818540361) * 10 ^ 70 + 5228591099280028991104288363257134890788490208435390470077722623567501) * 10 ^ 70 + 2158823854540521586616494063076345916660369017930859421679481936858556) * 10 ^ 70 + 7403140628401945779833982459436478509212668265952740251402356611007462
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_392 :
Polynomial.coeff recurrence5Scalar0Exceptional 392 = -((((1061168075422358459703778 * 10 ^ 70 + 4218763869607527299928823954158561585002048628700376071590013839926162) * 10 ^ 70 + 8693782527817322045455265509238114704533079165506783152647300000507008) * 10 ^ 70 + 8071780222235051045518236893800092573338705844286190541150337215894630) * 10 ^ 70 + 8869380715481310974197855246423514269372705374439232949044342440275558)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Exceptional_coeff_393 :
Polynomial.coeff recurrence5Scalar0Exceptional 393 = (((301010381383318213134657 * 10 ^ 70 + 8814673231089049479094781391446383021458184833787119902436878634254770) * 10 ^ 70 + 8672243180861193602700325147916794115819028780848825418595999119677665) * 10 ^ 70 + 9038246821782433914351374880741484164137533014810113702468408344511808) * 10 ^ 70 + 1632783777245059125958053777550390738184606358481760902133413485366457