Recurrence 2 lookup certificate: Scalar0Main coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_197 :
Polynomial.coeff recurrence2Scalar0Main 197 = (512543809503711841059539719243599893553308504354712687203379143 * 10 ^ 70 + 1790082514576770805393640092359503711341353412346217001852999469286684) * 10 ^ 70 + 3308704942805971465723623076506669453611878610444512571483566225477886
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_198 :
Polynomial.coeff recurrence2Scalar0Main 198 = (1619447353792636702998926731538572792488540138925222772371547266 * 10 ^ 70 + 3212160027254596726962134141423074256956448020497882790705894846282829) * 10 ^ 70 + 9221972002505453659101992048149600978772496315449316989225991101211217
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_199 :
Polynomial.coeff recurrence2Scalar0Main 199 = -((9502803458120758331571304939676827310213680939678240457611524453 * 10 ^ 70 + 5115753418352870130547398265621104623861870771294053254954303907729057) * 10 ^ 70 + 6101248561811073050500385538752745398047792798931969251265154439118023)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_200 :
Polynomial.coeff recurrence2Scalar0Main 200 = (27138426003291213106867284727220966873626730229651138311721822755 * 10 ^ 70 + 9438705111871720824306244666160196308039459775079310275496277598264695) * 10 ^ 70 + 2139878955924993213353816502413363649833637697107825433550632609286400
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_201 :
Polynomial.coeff recurrence2Scalar0Main 201 = -((48763698208382335263726808135302600849063752874068423737250989081 * 10 ^ 70 + 8277825315305486214415422178205005380985636591133981519834187477850277) * 10 ^ 70 + 719975022079909990063826708564977441410263259039788563051165161420693)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_202 :
Polynomial.coeff recurrence2Scalar0Main 202 = (30314950455465665832091264378984030424552642151107226292122861560 * 10 ^ 70 + 4575011288946916923801265952030142826003943679013974376058395491149772) * 10 ^ 70 + 664407342166385036816282693864888376433450248122124738785513923686850
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_203 :
Polynomial.coeff recurrence2Scalar0Main 203 = (163250864039074833868464283153990068148764346978848591960909451825 * 10 ^ 70 + 4819316822714699230560681188899814953176463557588240264235392305109466) * 10 ^ 70 + 3363336221692738056908677177808155154852008889667221660194688264074362
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_204 :
Polynomial.coeff recurrence2Scalar0Main 204 = -((806544082957949124219042041917766128151394845559920579733340316855 * 10 ^ 70 + 8108836133443980462058071232424760817618645787161342065476609527143922) * 10 ^ 70 + 489720745964022892300851121487424376278833463690434541754456405711662)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_205 :
Polynomial.coeff recurrence2Scalar0Main 205 = (2230494282487526142703925274781293701203421199729424709712984317796 * 10 ^ 70 + 8909182036390470711247434943562605887742458747624507046363932071768786) * 10 ^ 70 + 4700126460679039476662599812081005211005512811540179396405711124492942
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_206 :
Polynomial.coeff recurrence2Scalar0Main 206 = -((4282590052405085668240657082446982244942539025528054776537071598376 * 10 ^ 70 + 7453605234242746284640913057339399968671856384720620944733249895344187) * 10 ^ 70 + 3517104756551522023315025315658286872573237104364584616135789958531283)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_207 :
Polynomial.coeff recurrence2Scalar0Main 207 = (4750593637605217934411486677396311239170982210461508917960720287008 * 10 ^ 70 + 920875569099924873119311502350286741691762968247211728394282281735112) * 10 ^ 70 + 8043145955023500116526487246211241756887177227118776823349416546365547
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_208 :
Polynomial.coeff recurrence2Scalar0Main 208 = (3891440956485842246256885780864644536116918674753338618093911103376 * 10 ^ 70 + 9963346093014245595705825072573063394146189976281065764236858187781085) * 10 ^ 70 + 5502030608161634655885828078254100967130683140699734664221732857174285
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_209 :
Polynomial.coeff recurrence2Scalar0Main 209 = -((39242350204705210747298165352624941404762179039387598936473411975956 * 10 ^ 70 + 3589887789799085335748701257109411966862883943829488518190542103857612) * 10 ^ 70 + 4151639228609766352226309574530947991552029722752704293843952229047310)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_210 :
Polynomial.coeff recurrence2Scalar0Main 210 = (132078702326884389572161696181358489019681411665019578986768625352702 * 10 ^ 70 + 7759106918943047912654206813354368138552278617048169746717937693698938) * 10 ^ 70 + 5201997904702091226548789156159273843536318331315614776453997475860658
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_211 :
Polynomial.coeff recurrence2Scalar0Main 211 = -((317657295732530095977004763914703172430214563849924064772425230961686 * 10 ^ 70 + 1535778253431585095323004618440645760021771299291824648403704864788297) * 10 ^ 70 + 2525931027258889892760047175471191297323135703162751063316404553670549)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_212 :
Polynomial.coeff recurrence2Scalar0Main 212 = (592507382461223672898893151936669426821587802136287449300757929184144 * 10 ^ 70 + 799980127151673622814726367666979838187131364743663241164789965549170) * 10 ^ 70 + 3642309178140446090458114859442998112560080362379769366663361082370987
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_213 :
Polynomial.coeff recurrence2Scalar0Main 213 = -((796493968741677396506071901750975789410107568649343390605726255883350 * 10 ^ 70 + 3272980246804241553281307921342720589100886691610170305721119907614265) * 10 ^ 70 + 1936101958156895146533802262435622096584671660623207513409840115789808)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_214 :
Polynomial.coeff recurrence2Scalar0Main 214 = (363455838429281447432520151926672528076015611149620836027991153929566 * 10 ^ 70 + 91141540218310626769339018013628104726114481167295634851178491514613) * 10 ^ 70 + 2160137053375464841090319735951968186606132384216178086829340217445081
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_215 :
Polynomial.coeff recurrence2Scalar0Main 215 = (2116804250504527762223776718573470200309487281378073655523891614735427 * 10 ^ 70 + 9815402572409903340936165108845388540995589357071502120406040121599813) * 10 ^ 70 + 8748265183983318298862604064233897357259547176670654766155115427105448
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_216 :
Polynomial.coeff recurrence2Scalar0Main 216 = -((9541451845983921418015633653398907090824329314366918286829591695420225 * 10 ^ 70 + 698006543281905809324064544291941702029269882267460934859639933912908) * 10 ^ 70 + 1572734452531367168546425326888772394323152188925167440904311784933852)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_217 :
Polynomial.coeff recurrence2Scalar0Main 217 = ((2 * 10 ^ 70 + 7044135839114358993029359919257407773744732231460666962748967161692942) * 10 ^ 70 + 4775579754645322130520624417277856803836007847436503686472226785573749) * 10 ^ 70 + 6776247096903083035867329979853398579219813129759465328574882151194681
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_218 :
Polynomial.coeff recurrence2Scalar0Main 218 = -(((6 * 10 ^ 70 + 2538967047282081821004930822668329564178279709386288839318492995053703) * 10 ^ 70 + 3612365289085911496526414956916778114309304338558181926390797750409800) * 10 ^ 70 + 3544379016712539350866106379955802522149141420440091521976232549447807)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_219 :
Polynomial.coeff recurrence2Scalar0Main 219 = ((12 * 10 ^ 70 + 6439066589252220239128087720391064117766986428728711619462746074248723) * 10 ^ 70 + 1684254522463313285999884996816366794595754628787882372839767529901127) * 10 ^ 70 + 6129066646801823096495781456302815636735894219580251900623037318553813
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_220 :
Polynomial.coeff recurrence2Scalar0Main 220 = -(((22 * 10 ^ 70 + 9593397308996101828504449833599142402540079844017306385526294173139221) * 10 ^ 70 + 2014905060329964058462530104408083490161648848595340788344450755161971) * 10 ^ 70 + 2416139441024971620326033838648014087732165750260196507615683255044859)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_221 :
Polynomial.coeff recurrence2Scalar0Main 221 = ((37 * 10 ^ 70 + 8267552489233198117958156125016027818170873831241827737875792890059303) * 10 ^ 70 + 5665685288512651629343720437410466754723436243053192379751484819455413) * 10 ^ 70 + 6251588826920821035390245443466786793936003956943084979465411175354490
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_222 :
Polynomial.coeff recurrence2Scalar0Main 222 = -(((56 * 10 ^ 70 + 5115522048409354569149498399435580344911516411547118135201408957438311) * 10 ^ 70 + 1078921233041604114737325604666329744544164813362554891602835337926488) * 10 ^ 70 + 5955832313154847234104024110785523093186601409747742247883851970639920)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_223 :
Polynomial.coeff recurrence2Scalar0Main 223 = ((75 * 10 ^ 70 + 5788857859565195826551753360670762524504062217065205363657435637230656) * 10 ^ 70 + 4940818025556161167993458344833649778662619790417827587208090577587802) * 10 ^ 70 + 6745968556519435388020747046996093480649170452915055185491072357463871
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_224 :
Polynomial.coeff recurrence2Scalar0Main 224 = -(((87 * 10 ^ 70 + 2252601188096239956345822950677259059215519921121583733475619994267507) * 10 ^ 70 + 6661552127377246646430148391195555870384959033402913393661644364379595) * 10 ^ 70 + 3074376134042007850141282420068400883331173183939127237592947046576190)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_225 :
Polynomial.coeff recurrence2Scalar0Main 225 = ((77 * 10 ^ 70 + 5933970461636268309473880911283474144993296272809546748981352231100969) * 10 ^ 70 + 1935566419895195922550305557545089185444871211005115145734818348874789) * 10 ^ 70 + 7766884754548167365894705279279490951538735439319628847900133991299469
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_226 :
Polynomial.coeff recurrence2Scalar0Main 226 = -(((25 * 10 ^ 70 + 6078765673983019972693586676741668159288599131656452671979729806558153) * 10 ^ 70 + 428163219460405467096942511708506054868656488341879321148573109989109) * 10 ^ 70 + 1577905614899222190024729196581539252157586114822909585366054031136298)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_227 :
Polynomial.coeff recurrence2Scalar0Main 227 = -(((96 * 10 ^ 70 + 9672335858234332120276697690791020921575890710730077923567836365593551) * 10 ^ 70 + 4220998879772604200834349402429005631802727737737331698314434361030027) * 10 ^ 70 + 1491576068254013301790920757117224829670723390819788018229550598119510)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_228 :
Polynomial.coeff recurrence2Scalar0Main 228 = ((323 * 10 ^ 70 + 5455236209801424610041435857794449550698297753882092810500358181051908) * 10 ^ 70 + 4862081396301230589760872013070860107126658928474316566068483903791139) * 10 ^ 70 + 7527840334643789797052081708805664721101153027499153674146158291949379
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_229 :
Polynomial.coeff recurrence2Scalar0Main 229 = -(((688 * 10 ^ 70 + 3527544025375376708662954634292833355128301300388723997055376185069115) * 10 ^ 70 + 7609223411657174185782757905863084079443216219432825051119953285814959) * 10 ^ 70 + 3989270870057328343039452379404802047644896669379371387630778687174335)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_230 :
Polynomial.coeff recurrence2Scalar0Main 230 = ((1219 * 10 ^ 70 + 7419526177743481023114519374405427627524231051376201976010109397736349) * 10 ^ 70 + 814381942232088147396429503047721117146722999671362984436367290989612) * 10 ^ 70 + 1284206151867546401623162905321900199415567033334377752558603318206497
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_231 :
Polynomial.coeff recurrence2Scalar0Main 231 = -(((1931 * 10 ^ 70 + 9775546212692469152463269242029469807897860589010600419960718070433207) * 10 ^ 70 + 8250197724177131728735357557546204984915701365461379496445603656179019) * 10 ^ 70 + 7654508671113161442739801517340258362730248678641276071571674754970312)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_232 :
Polynomial.coeff recurrence2Scalar0Main 232 = ((2817 * 10 ^ 70 + 295988678013253409163933522864067461773760504267117075990684960914462) * 10 ^ 70 + 7669641792510907336541756721339511894115184229384238946340784312801879) * 10 ^ 70 + 7311836215902119111258904866591548671781764857938786452225287840910362
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_233 :
Polynomial.coeff recurrence2Scalar0Main 233 = -(((3838 * 10 ^ 70 + 4473875765882953468411278992795376291041440610849406368768812805798214) * 10 ^ 70 + 4286792638022729688586007372284338219952823707501476968888486810856871) * 10 ^ 70 + 7354383957617641737184101715960457586542999588868229037534821336045059)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_234 :
Polynomial.coeff recurrence2Scalar0Main 234 = ((4929 * 10 ^ 70 + 4368763117735551828559682002406263335004923530953242705717342925338493) * 10 ^ 70 + 6100946441501695072451523700190378913619691322455815441029712959762428) * 10 ^ 70 + 4936829260051910850926350584238525733570343838517004723417103719249988
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_235 :
Polynomial.coeff recurrence2Scalar0Main 235 = -(((5996 * 10 ^ 70 + 6977061976955231560115705808862635910987540626833836465651591019392047) * 10 ^ 70 + 2055458738780199586624367727987362618885488527166923057485094367205854) * 10 ^ 70 + 4697327418380295987151912663377008082480773236450417185893581112627223)