Recurrence 5 lookup certificate: Scalar0Left 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.recurrence5Scalar0Left_coeff_307 :
Polynomial.coeff recurrence5Scalar0Left 307 = (((134577079616470379205841806964552560470673877884719414144152178 * 10 ^ 70 + 4931330279372412897087546809964997531804621428998358744259518887863146) * 10 ^ 70 + 6167818270993043560560800650783416226542956317362210951280800930448718) * 10 ^ 70 + 1643823394379510407640272357600569407809748193721576218340867219509164) * 10 ^ 70 + 958467544157221122786148080979252990420332052755040214575477283155149
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_308 :
Polynomial.coeff recurrence5Scalar0Left 308 = -((((65695228550390140827279717588632375922457460071097172058860978 * 10 ^ 70 + 6603795432797210872335369294489136479482076501582614484023555772085080) * 10 ^ 70 + 1990686743201499362632184642209664557879868628587762389185108857285336) * 10 ^ 70 + 5161550548943319047363304055352611999851715928902378591630056635270386) * 10 ^ 70 + 2190376001497461661764015911319633392796859687031434057144126989785268)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_309 :
Polynomial.coeff recurrence5Scalar0Left 309 = (((34057369510311176213951855504200712636521482395929029028003179 * 10 ^ 70 + 8465131667263863564856511692214151745695289387075256021910568011224931) * 10 ^ 70 + 3224420143679990246655259748463066636897518340006322565715059496641723) * 10 ^ 70 + 4177113854596779607780242817497045607899501098381939187834183077726943) * 10 ^ 70 + 478440625008682294414414592717769541558739851399324771588377158990897
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_310 :
Polynomial.coeff recurrence5Scalar0Left 310 = -((((18366096495656180361663393535530947176993687258948212598338470 * 10 ^ 70 + 9278934232402859898149087274093176049981802878730768806949730269223354) * 10 ^ 70 + 791105175846733732782078137493827313706279082868551044335328303237541) * 10 ^ 70 + 2171264780678884877814126730600645363932290254497330650759186913571196) * 10 ^ 70 + 878628582001800258638073388561006241756640359109936000830090615835526)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_311 :
Polynomial.coeff recurrence5Scalar0Left 311 = (((10042270539578829328674788880456400636162720981013141905479731 * 10 ^ 70 + 5994368270217661521614199379617762839870388330073406459813097290327053) * 10 ^ 70 + 9511905581739181345914482097146620958872137481981872905066826009029994) * 10 ^ 70 + 864985045104535699543037536641001829691664664893124300053323170963442) * 10 ^ 70 + 9928904112919422137781358271570875071573923305190029152181226888275172
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_312 :
Polynomial.coeff recurrence5Scalar0Left 312 = -((((5452798881221061159256913954499108078817763485277800428332793 * 10 ^ 70 + 1130259417537121629066397359083255062984780316489890997632225983310439) * 10 ^ 70 + 8007191939785312138318409702694111438514711769613184329541035402446312) * 10 ^ 70 + 2167057876813215051383143339245877190302636792299428226101583563216001) * 10 ^ 70 + 3232710875822936818610836937067872589387014267800405417452374727930368)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_313 :
Polynomial.coeff recurrence5Scalar0Left 313 = (((2901110380642133921172074926667308103446808433256222397483275 * 10 ^ 70 + 7007781007949147582088712092177441873252246103726631852253562969976439) * 10 ^ 70 + 7923853368554501206142467609598586261849284929607536715191388764886048) * 10 ^ 70 + 3077850230021231976585520716699743217213568208944080277222157787997105) * 10 ^ 70 + 5110672456617830256750856777482426993471093548248912950896610213436386
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_314 :
Polynomial.coeff recurrence5Scalar0Left 314 = -((((1501339106208967045813265633044432220404088270783025024889395 * 10 ^ 70 + 9048596688662889881250173043421831509461944914183734252458520100363689) * 10 ^ 70 + 3564393885326248589988887798816135133074431450781765514841790529669998) * 10 ^ 70 + 1047779414580563572927748014869145675970408216689944380448575777988353) * 10 ^ 70 + 1953472128578945304839315697258750541340440048219761702578635607658983)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_315 :
Polynomial.coeff recurrence5Scalar0Left 315 = (((753162437551918733032035120857509112931343435411936175080995 * 10 ^ 70 + 7061104731468507146243964276314167680136243344353709870517723813514135) * 10 ^ 70 + 2582266294735334738813324180173202431321332346959168784505534362322461) * 10 ^ 70 + 2739388278611326088527943014532989662578684717747721206074710260187024) * 10 ^ 70 + 8977345540626001081853696072919541494425728160971272880178239132439502
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_316 :
Polynomial.coeff recurrence5Scalar0Left 316 = -((((365882682161826176130870757780208920198879392970154999065326 * 10 ^ 70 + 4653348662399730885221370115731795155154795252466204672631150934589547) * 10 ^ 70 + 4251901631383299555684226349486617874306619840677823696366692166925749) * 10 ^ 70 + 5317993370146697195144227158139896106769267318590979944598235922945799) * 10 ^ 70 + 8207172380860477146452438027940652745306699408482456306938305723431970)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_317 :
Polynomial.coeff recurrence5Scalar0Left 317 = (((172188645288150684092713914189092213302817576653535914390097 * 10 ^ 70 + 2912676664917598886590322142629583594598138530211521509952319999620176) * 10 ^ 70 + 4639670260800498235388821203161758465201300056008975483101607263302764) * 10 ^ 70 + 9030541096309955346493154087844324424851028896091640407059981718452947) * 10 ^ 70 + 3083966497379281282421643069302575561036302845909441958335111245099681
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_318 :
Polynomial.coeff recurrence5Scalar0Left 318 = -((((78609398021883278494842019243187341376222538627123461634610 * 10 ^ 70 + 1245648980496091639330475477158922142137559724538156179138248437244073) * 10 ^ 70 + 1750972396355671207100066033441237481664301988405096857239586171827957) * 10 ^ 70 + 1040677195965556697667513743364485872392610807957323587916358825664761) * 10 ^ 70 + 6724119566035045637018734158724577156703840491112092434378293871335700)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_319 :
Polynomial.coeff recurrence5Scalar0Left 319 = (((34893680293938895296427574243208802458364832753197888303072 * 10 ^ 70 + 1449035966389106087399779839305784209804424934681974747925284657359171) * 10 ^ 70 + 1303405873310211099721186827243394757995928988843291946757097304428689) * 10 ^ 70 + 5916924777269193906631716125489025045844829024325576896498031280302098) * 10 ^ 70 + 6600051355996812082662576626242418192420706344444929406873518743782506
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_320 :
Polynomial.coeff recurrence5Scalar0Left 320 = -((((15110848263714219305750960935959822350881373204801215079897 * 10 ^ 70 + 7090341472062985329678193387010573644781639273657710579219726353708907) * 10 ^ 70 + 1699142105610401764855661639419539108688992526652016629363471576350186) * 10 ^ 70 + 7725509542785432499773069833930899550747239224612204746552727522031449) * 10 ^ 70 + 5612127785806253121636657398067388218225373666369700240113887343125542)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_321 :
Polynomial.coeff recurrence5Scalar0Left 321 = (((6414969816237585136236875430020513893984480426951665833974 * 10 ^ 70 + 3683527400222968248763189230890555251434100839225249021960623875846147) * 10 ^ 70 + 911256360282167475675045006524948146876810710615034274927144605784223) * 10 ^ 70 + 940853286254439797023759537095104686820968042898086540956336514728389) * 10 ^ 70 + 630851858778316738960945574800315693712229573520111029047004945499624
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_322 :
Polynomial.coeff recurrence5Scalar0Left 322 = -((((2687631572727858780907933911324609107063279741599704811960 * 10 ^ 70 + 210829144293370375522987355764433902853236228336463995923593667381946) * 10 ^ 70 + 5175963704676198273799191858866098185806205615640312733561954850349359) * 10 ^ 70 + 678720037386992170724834281674049152798534839997030699534435550407430) * 10 ^ 70 + 9468366672984841986585790555718386042472182198278128761093921571015792)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_323 :
Polynomial.coeff recurrence5Scalar0Left 323 = (((1121095443700394660445838530504904913237418068139704078278 * 10 ^ 70 + 9910184730097808558931522098997419223513432285874126659082883828575930) * 10 ^ 70 + 1239315171132872382781967880399148410632224276993027503574018019256154) * 10 ^ 70 + 8757628505660437190931438809467965288207629606115784962034409886520709) * 10 ^ 70 + 5965724529752939586217511641928312220771480417915092361818442319424682
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_324 :
Polynomial.coeff recurrence5Scalar0Left 324 = -((((470554331284581195464846744122346923840556077106089900634 * 10 ^ 70 + 4113988279670499920573990938262458923514083045259607469563847144090592) * 10 ^ 70 + 5352275358834734442434829879034102483162688320502240886562233917407052) * 10 ^ 70 + 3729974170431126860963018212996177222269255837715988875751440051141608) * 10 ^ 70 + 8581731002233440685910182730917455726878012661790001435711973493511388)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_325 :
Polynomial.coeff recurrence5Scalar0Left 325 = (((200906573797128150799410248316976266993667748914125155995 * 10 ^ 70 + 9289779414400737599383854436935184065017972168562754132433433212901152) * 10 ^ 70 + 3430054305384327123877458717739528616724342849361780690873416934123350) * 10 ^ 70 + 6732287459182069076160126409680069681836851714024762460355392797934380) * 10 ^ 70 + 1550657891306656228835704772427976036156899934050052833335465807674973
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_326 :
Polynomial.coeff recurrence5Scalar0Left 326 = -((((88001946713976769573678920369687817367064129703553056428 * 10 ^ 70 + 1524728019635675496003101414020948985372060214710610510935966060195549) * 10 ^ 70 + 9083175214943168277672322477136982210771030563078604595683533807086915) * 10 ^ 70 + 9229083453158197258083679068291094762534507820096909871890000849594196) * 10 ^ 70 + 3553603387437330118686374920959902486464542773040857848897732094669700)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_327 :
Polynomial.coeff recurrence5Scalar0Left 327 = (((39679076713899295660939153937979380766537386851034523773 * 10 ^ 70 + 735996204632218242356280147527530761023188524716402560631411672089630) * 10 ^ 70 + 387080900143704393092427454012374299648630256834339709696379246069902) * 10 ^ 70 + 3286952787445175176263295979169192181671567360810626514761851897635429) * 10 ^ 70 + 2402821013600653157788843424894172324598948494619295379353651082206793
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_328 :
Polynomial.coeff recurrence5Scalar0Left 328 = -((((18362012124147845426059635478257687770847830186477067360 * 10 ^ 70 + 7363360145978741334067140626938818977008503433963527563426264199048530) * 10 ^ 70 + 8466364176457480793091025392505133284770877055099272000350207761568603) * 10 ^ 70 + 4268797931239814732772155604082331417774909291393604749828493349296675) * 10 ^ 70 + 3643969545803823003496033318611990994926476795225928165262370865826596)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_329 :
Polynomial.coeff recurrence5Scalar0Left 329 = (((8652476086588773003731182123923636774346483832403703229 * 10 ^ 70 + 5251022961846433106158649443962737492746459801116346572744525658464161) * 10 ^ 70 + 2539420844885028299318043204038042867208023888342359629144546866270613) * 10 ^ 70 + 6530343936099762610092195753433612980374150311763480400602400861699563) * 10 ^ 70 + 6496461398081881531982332418347627671789884646727962008853096764016592
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Left_coeff_330 :
Polynomial.coeff recurrence5Scalar0Left 330 = -((((4110452857555212153407741051208641014994583272341626358 * 10 ^ 70 + 606776806454625532992493478581594152852198682928734824668804779526393) * 10 ^ 70 + 4246462375087927903581328834614802838616872088952498209709012762594916) * 10 ^ 70 + 5802337438679156875131194024996875374984195279536010642772561852441224) * 10 ^ 70 + 2586243499102382297462294351591085922203886427627481767953922350394187)