Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1LeftPart0.Coefficients93To144

Recurrence 2 lookup certificate: Scalar1Left 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.recurrence2Scalar1Left_coeff_93 :
Polynomial.coeff recurrence2Scalar1Left 93 = (58827786 * 10 ^ 70 + 4432406129800774748573646224325706075461829078396926021275319512776582) * 10 ^ 70 + 8906252271144102999124906700809315502248828714058450203850278218065695
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_94 :
Polynomial.coeff recurrence2Scalar1Left 94 = -((268974026 * 10 ^ 70 + 7794696292268061596290829201028004683688670117923165775068359629197602) * 10 ^ 70 + 1320700101329068814843826020479095928194307759561248941928147062622957)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_95 :
Polynomial.coeff recurrence2Scalar1Left 95 = (1179356278 * 10 ^ 70 + 832246569275813152270076524823531042593473324199488443272691540874834) * 10 ^ 70 + 7521132714772023173653439041424259868083939760695358050437241238184007
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_96 :
Polynomial.coeff recurrence2Scalar1Left 96 = -((4951589539 * 10 ^ 70 + 5063573083873226737676670180735184224253718721123490567511676525606642) * 10 ^ 70 + 4772530887887269219957720565354307039678583124351501391359479393507041)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_97 :
Polynomial.coeff recurrence2Scalar1Left 97 = (19856243849 * 10 ^ 70 + 3610016663755781949512429201338684598725890351843090320101442835809032) * 10 ^ 70 + 2900276801078865547528500218284276599670917825088585990981926553059310
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_98 :
Polynomial.coeff recurrence2Scalar1Left 98 = -((75715641249 * 10 ^ 70 + 9502978594245802834804203255843643843936254725800898257557304926640044) * 10 ^ 70 + 838922612020177368812675188114906036430977285987591804340100030020855)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_99 :
Polynomial.coeff recurrence2Scalar1Left 99 = (272560292616 * 10 ^ 70 + 3698661086247701156764393307744555336948143854358382314774428929317053) * 10 ^ 70 + 6233796250038026575727413860472821236378019458794461095045464435084025
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_100 :
Polynomial.coeff recurrence2Scalar1Left 100 = -((915694116826 * 10 ^ 70 + 3665172799764213648695879602970168181571868982088690389315686044832402) * 10 ^ 70 + 4405298452732843899826799941091108928264452060994387208142795236758342)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_101 :
Polynomial.coeff recurrence2Scalar1Left 101 = (2818708373261 * 10 ^ 70 + 5046714191163118772468168596516001896036883590375324459257557473389294) * 10 ^ 70 + 7359756138577470191740645193879617058550050286139567594657599313075458
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_102 :
Polynomial.coeff recurrence2Scalar1Left 102 = -((7690128628719 * 10 ^ 70 + 3862913796108494628476024596423416557394652811168777304770478896726811) * 10 ^ 70 + 7441601881734677547328058651689143891038680696783066592068566782309507)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_103 :
Polynomial.coeff recurrence2Scalar1Left 103 = (17192412077097 * 10 ^ 70 + 9692904328903721100704860646442652015478295485311314374887003763671042) * 10 ^ 70 + 140334184272964381036911811251834888806882341766108362340625646999696
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_104 :
Polynomial.coeff recurrence2Scalar1Left 104 = -((22632705884759 * 10 ^ 70 + 5238900286917122428342203822815680365565366464404227784808573966787417) * 10 ^ 70 + 2060063193437826535909029155649890187734062108186934232352131679836114)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_105 :
Polynomial.coeff recurrence2Scalar1Left 105 = -((52395636312396 * 10 ^ 70 + 7457690939279865454142327798692615479740764916361155138233996313083275) * 10 ^ 70 + 4557989667305692605105040160852099504521967218696893948270536028689497)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_106 :
Polynomial.coeff recurrence2Scalar1Left 106 = (624780238039003 * 10 ^ 70 + 5956546833549355990692783448531433269119129888785005083509333456832460) * 10 ^ 70 + 755623788444407903192946673895439120193280963598947668332254751254725
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_107 :
Polynomial.coeff recurrence2Scalar1Left 107 = -((3666462208845041 * 10 ^ 70 + 7475854423234724957197799673540926083006012805223607176862296219139504) * 10 ^ 70 + 7952345063340440561821729317141670120995137659334324224633862273233394)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_108 :
Polynomial.coeff recurrence2Scalar1Left 108 = (17699509765584951 * 10 ^ 70 + 3673972515220027136150598914727182688839732888948144763848650515976917) * 10 ^ 70 + 2161724417850701647573793848296201509011083859464713130968710872110449
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_109 :
Polynomial.coeff recurrence2Scalar1Left 109 = -((75464422261107684 * 10 ^ 70 + 2784835042228810060226667975219026561956895319918132674940445760266226) * 10 ^ 70 + 2618156307766564363404816340912153288045602854696109757627612010348653)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_110 :
Polynomial.coeff recurrence2Scalar1Left 110 = (280035898720168084 * 10 ^ 70 + 5386235770214955657569489177197003585162502989191036734435207393076183) * 10 ^ 70 + 8444898991458056590534924861247805274483785004292374188953190558663650
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_111 :
Polynomial.coeff recurrence2Scalar1Left 111 = -((845481429395484670 * 10 ^ 70 + 1615825311934108569503681796131857217430914497596182693318545047994927) * 10 ^ 70 + 3951061268091868549067474994991041388345312953297284905612920217267154)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_112 :
Polynomial.coeff recurrence2Scalar1Left 112 = (1724830628753702886 * 10 ^ 70 + 124272626654457115268226149121514988912539809133437596769169727004078) * 10 ^ 70 + 3242918568040454618380923004871308177496674956801461977756762480378532
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_113 :
Polynomial.coeff recurrence2Scalar1Left 113 = -((310866113768011547 * 10 ^ 70 + 450101378607235760365493984799974527053927345503418661978301819716674) * 10 ^ 70 + 7680628152764502355648009444353700059929997664359899188427828772826677)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_114 :
Polynomial.coeff recurrence2Scalar1Left 114 = -((13208303979746668378 * 10 ^ 70 + 2200042674839423524511229303857503984932560794054223433661961109384872) * 10 ^ 70 + 9331049231648201940975586957997367717911884794555686904495828503859101)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_115 :
Polynomial.coeff recurrence2Scalar1Left 115 = (34967296148304676835 * 10 ^ 70 + 8801768736474968981893191709294076719930098814524901893970445516145991) * 10 ^ 70 + 7090520676818662430466129567959446227410020870489151017889438048448204
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_116 :
Polynomial.coeff recurrence2Scalar1Left 116 = (169747731020044184023 * 10 ^ 70 + 3196816149809601874654962733960156653580186635810174211131049595233170) * 10 ^ 70 + 2439738970147583095772049538756849036178131810223796452971528466757598
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_117 :
Polynomial.coeff recurrence2Scalar1Left 117 = -((1952720754649723920342 * 10 ^ 70 + 3904033485448048381540033402274760354365452151289145975796009338531075) * 10 ^ 70 + 8872192464306308884532561057949485229908122578706770990953208288274260)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_118 :
Polynomial.coeff recurrence2Scalar1Left 118 = (9039902728894179916864 * 10 ^ 70 + 1263050718232424486885229576046665258753497685220233756496268614347719) * 10 ^ 70 + 2471214133722720782749123327584570862208078892688503725783375176528821
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_119 :
Polynomial.coeff recurrence2Scalar1Left 119 = -((19531281723726574033876 * 10 ^ 70 + 3615317205525252922993647210532098462646670742550803934836442668175893) * 10 ^ 70 + 5060781675875647497631006278743434114248550063786357349531425856093179)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_120 :
Polynomial.coeff recurrence2Scalar1Left 120 = -((41343140460340923182745 * 10 ^ 70 + 1481715032631220400331740291591787098741801898720115086245739622348433) * 10 ^ 70 + 4519538750303173493840870349340627291619490370715117626670631083800004)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_121 :
Polynomial.coeff recurrence2Scalar1Left 121 = (585223115787761262306295 * 10 ^ 70 + 7345649998346465818872888866983813482800719291405468654347874926478839) * 10 ^ 70 + 2549679906297147039613422168348784785771887801163456407447840923318839
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_122 :
Polynomial.coeff recurrence2Scalar1Left 122 = -((2870552622634118107143994 * 10 ^ 70 + 9474245991050488131671121134302868843852786536220548864686642243847352) * 10 ^ 70 + 6490812431968605072387475131496481163664081091145903487683462913060471)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_123 :
Polynomial.coeff recurrence2Scalar1Left 123 = (8076916298941546341083877 * 10 ^ 70 + 5441180495839473007439131428325160327144791381111307056605300398797105) * 10 ^ 70 + 762040047163092640989117183826340268415379630069053623812929153366693
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_124 :
Polynomial.coeff recurrence2Scalar1Left 124 = -((4867718824484632258250767 * 10 ^ 70 + 4704280562182954033924446358077260316721080360856915571835460369858799) * 10 ^ 70 + 9715672176313101391356137482889547173394243668690761397061650007486605)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_125 :
Polynomial.coeff recurrence2Scalar1Left 125 = -((86288230161021754549433108 * 10 ^ 70 + 5681000090790968184430344098280616947825482951960889177326433048901490) * 10 ^ 70 + 4668554592436450750958200368363647133139225435157254202134394787886853)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_126 :
Polynomial.coeff recurrence2Scalar1Left 126 = (545914832944138431445519466 * 10 ^ 70 + 5238567442471117053599510868833318715500725677845565607038307118239654) * 10 ^ 70 + 9230107622888619061429610031881314784006099947758941510845574444396485
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_127 :
Polynomial.coeff recurrence2Scalar1Left 127 = -((1869365973441287947418382750 * 10 ^ 70 + 7229039846632643349627727979045022083703167545474034393069261832644400) * 10 ^ 70 + 2321626941260221871432870765565521749989853811563617745458315103658833)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_128 :
Polynomial.coeff recurrence2Scalar1Left 128 = (3622327811371649007032362568 * 10 ^ 70 + 9828432710467789033889134231431524643894571452157730127709654369239634) * 10 ^ 70 + 6624073148685048620075180796312113487920767612225687047821916344025986
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_129 :
Polynomial.coeff recurrence2Scalar1Left 129 = -((385716782333403218279228019 * 10 ^ 70 + 7098978510872009906702478602474197815647236298699409398340230252744338) * 10 ^ 70 + 3609531348388793532436557508756807383334234105580698874530381889801788)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_130 :
Polynomial.coeff recurrence2Scalar1Left 130 = -((27764707804767912443193856061 * 10 ^ 70 + 1525390368992226495537745958024209597451857540202945323922690568961285) * 10 ^ 70 + 8930416958082839138182276754249366225313405286196221678805320726410614)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_131 :
Polynomial.coeff recurrence2Scalar1Left 131 = (187725923978735769345393356114 * 10 ^ 70 + 7871685257667705876556189633683463544802140368150682684470253922164188) * 10 ^ 70 + 8659674594374807574619328358222918059228298847560504770451741777685525
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_132 :
Polynomial.coeff recurrence2Scalar1Left 132 = -((1255537463073816627690964709496 * 10 ^ 70 + 358670084165800723221297300053868349623069561301538077775496585520429) * 10 ^ 70 + 8981068935262903894733740131398588818660360138902005623521492000690787)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_133 :
Polynomial.coeff recurrence2Scalar1Left 133 = (6878471295454154081282507104375 * 10 ^ 70 + 3775971198692753578158441407802699239178098990861863990697541523040661) * 10 ^ 70 + 507802683272814198294097759135014590943737892666552192513590270365602
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_134 :
Polynomial.coeff recurrence2Scalar1Left 134 = -((22351089418848162812481856621437 * 10 ^ 70 + 128014598096167835757137877589973612570548069211231875834996272791187) * 10 ^ 70 + 6612721906463663578539223700670762843179202443985481555924875491504022)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_135 :
Polynomial.coeff recurrence2Scalar1Left 135 = -((1582714238207805479261439382984 * 10 ^ 70 + 7836531102875863454479387133392412916045448860707014783228882520537615) * 10 ^ 70 + 1063776439858500615072829640734977673271314086786814243343343007250947)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_136 :
Polynomial.coeff recurrence2Scalar1Left 136 = (440112010991455288111330912136610 * 10 ^ 70 + 2245507660140772756280040498200988543778714113532553468867678508967791) * 10 ^ 70 + 5389735840693694004755938340618642643559331832527702835228900451090677
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_137 :
Polynomial.coeff recurrence2Scalar1Left 137 = -((2334500998518826489246603433969813 * 10 ^ 70 + 6783458769458693586900915695621087079847689843554377293319201311830335) * 10 ^ 70 + 2391094028710648432839165917714463446209898444123756245071560072767502)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_138 :
Polynomial.coeff recurrence2Scalar1Left 138 = (4649031313326225205289398230376719 * 10 ^ 70 + 2468772059077008742955539647208901488729883912146755696135275558675648) * 10 ^ 70 + 238754474345751469011054849011349059794458498702204358071468983718477
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_139 :
Polynomial.coeff recurrence2Scalar1Left 139 = (11951121004976412944500149983293480 * 10 ^ 70 + 973192255074896872128794814515736755258294938922164990335995088636905) * 10 ^ 70 + 7255985075742362165532453808569301961656468656263141008402856449676766
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_140 :
Polynomial.coeff recurrence2Scalar1Left 140 = -((108870007957691461494930233051977530 * 10 ^ 70 + 3974471080343940417576259456715936380040508119904184023744042090920654) * 10 ^ 70 + 7764084818683876794750644131713856655638221519260837651871354869735196)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_141 :
Polynomial.coeff recurrence2Scalar1Left 141 = (253986497144733626297762883514245464 * 10 ^ 70 + 6561827160314965343620233559241339196607667820401462098699640319790864) * 10 ^ 70 + 6930375448346038976083305297894769252430027921432827963691519120489478
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_142 :
Polynomial.coeff recurrence2Scalar1Left 142 = (476235707580260228613125738759038888 * 10 ^ 70 + 3683118135256697637720149595508385532675141961664096021093830086021933) * 10 ^ 70 + 8716176116344130875756669286960014687665687443100855769576600879975467
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_143 :
Polynomial.coeff recurrence2Scalar1Left 143 = -((4804596440483754350614904255409220753 * 10 ^ 70 + 6972450919738188923245168213985088460821208849754637367166394553595025) * 10 ^ 70 + 1886612232307267270160184235696705045088436978718956467886092035458285)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Left_coeff_144 :
Polynomial.coeff recurrence2Scalar1Left 144 = (9613246269561793135712299789447652302 * 10 ^ 70 + 2559246390276963665610839420485833646661472077528803978457409765636282) * 10 ^ 70 + 7297569571949006795413292514278055497605011043179337088114186911346471