Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2LeftPart0.Coefficients158To193

Recurrence 4 lookup certificate: Scalar2Left coefficient convolution #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_158 :
Polynomial.coeff recurrence4Scalar2Left 158 = (((56 * 10 ^ 70 + 6602234807461048838365660753268266471014958582573746938975051409983092) * 10 ^ 70 + 9898254968579238437619258742522275674137042661891563682560219285682569) * 10 ^ 70 + 5538264277288728731734171654495304548211263721955907605458986268352663) * 10 ^ 70 + 8539396837192802109822972697098380885972314417747581971305328911589608
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_159 :
Polynomial.coeff recurrence4Scalar2Left 159 = -((((211 * 10 ^ 70 + 9177025983972570504704063482862915856374056525033648803802134727355268) * 10 ^ 70 + 2189846903037854890532924619139394362305484081755958987791054907502222) * 10 ^ 70 + 680033689913571229064580988398628758182677679211237944312823179594920) * 10 ^ 70 + 2782740530661817696253568239014584171143212051107815361316688361551374)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_160 :
Polynomial.coeff recurrence4Scalar2Left 160 = (((779 * 10 ^ 70 + 9943414229728036322621805506066282900972847553426712366495439157180994) * 10 ^ 70 + 4107479593401394896725224084440088509486330931545627454138069546213931) * 10 ^ 70 + 2971812363958023420281970468996377231683744457698690401623760194356491) * 10 ^ 70 + 4614026239481282552482175332391461826015403722301442651386163857992681
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_161 :
Polynomial.coeff recurrence4Scalar2Left 161 = -((((2825 * 10 ^ 70 + 4398891237828200239077468392181884185564867044914646013845312883617644) * 10 ^ 70 + 900862486934683779636327592584308883036793297498077221222181201874195) * 10 ^ 70 + 747457409892810701348628543244125018778589416460936509223298986564427) * 10 ^ 70 + 3252171386214804843761048211826580116571376271360478125117736289209604)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_162 :
Polynomial.coeff recurrence4Scalar2Left 162 = (((10073 * 10 ^ 70 + 6124641270802831583772904501439673377706248652097876613799350657848500) * 10 ^ 70 + 5835090415163331412498235055007352258928415475946346980500317758864979) * 10 ^ 70 + 7395067997675806616022332659142282170385619051140248031223647099109911) * 10 ^ 70 + 118993174709696072847231411902920936932735158368066470937751201483684
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_163 :
Polynomial.coeff recurrence4Scalar2Left 163 = -((((35352 * 10 ^ 70 + 6616007439792782837082519888640965759340614436438742466616403693200765) * 10 ^ 70 + 11210182429182820149732979660787862766221022041530378112242526163521) * 10 ^ 70 + 4047373898629213467023317351335924169652295883099607169847199967542493) * 10 ^ 70 + 7355244758555543131354817777324204643842892846284828299005321191391588)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_164 :
Polynomial.coeff recurrence4Scalar2Left 164 = (((122131 * 10 ^ 70 + 8421882186051354335206094945947441859703568355761733144416095470023640) * 10 ^ 70 + 3248308108632928469422604077791895214107079017764014258935346493366172) * 10 ^ 70 + 4490527793783041138211131616050293764715471251364983591866550552107967) * 10 ^ 70 + 8689723088772279742687274694410374447482448528721302477593183088846001
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_165 :
Polynomial.coeff recurrence4Scalar2Left 165 = -((((415371 * 10 ^ 70 + 6808598996206970753704523309469328250340290671090465887013423324163335) * 10 ^ 70 + 4049044811697322053457391564399809460741637056576194560170579284187682) * 10 ^ 70 + 9610046987572770507763630446463618924014304975110085748865806474581733) * 10 ^ 70 + 8806549214200826763146199853377851389479183208352004298772265189327665)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_166 :
Polynomial.coeff recurrence4Scalar2Left 166 = (((1390837 * 10 ^ 70 + 5214608046898660907391609291141060211717174631329148041946428671091450) * 10 ^ 70 + 8905421157699629734726849830508079816758170007420615567511445483319890) * 10 ^ 70 + 5143598775615148118197052363560990255792196845177419715995678322203935) * 10 ^ 70 + 190646328201038150210443030435662935739523989960850554956063399659050
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_167 :
Polynomial.coeff recurrence4Scalar2Left 167 = -((((4585396 * 10 ^ 70 + 6510416368421928858450817088384672226832429489613710023698337749738999) * 10 ^ 70 + 9345083985989080609833927713290443794124318666165499163163632935630402) * 10 ^ 70 + 2160818571318678985834265063320263660643471683378616347347791422670420) * 10 ^ 70 + 6636969795852454388494978074532141348249753170195623728888861201934868)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_168 :
Polynomial.coeff recurrence4Scalar2Left 168 = (((14885622 * 10 ^ 70 + 4130080461682958391464355822920826526028435390810959551616409783333614) * 10 ^ 70 + 7666567069083428690848067087111833380155954841390438115388772893647685) * 10 ^ 70 + 1103820877955763074972904827406697893265399593443329730603522595817751) * 10 ^ 70 + 1502076954524890744455590954014475460669328311091002523305137383666143
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_169 :
Polynomial.coeff recurrence4Scalar2Left 169 = -((((47585472 * 10 ^ 70 + 7525031231259433875308113006125022355493825698752652934012537507452535) * 10 ^ 70 + 3688934449697434308135592764226822911700259737738662837812852385627694) * 10 ^ 70 + 9911456408980001082194794269149256888654870759241769297268795113259151) * 10 ^ 70 + 3534648548824913788631863533812002763056465333569328987486321420501881)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_170 :
Polynomial.coeff recurrence4Scalar2Left 170 = (((149804879 * 10 ^ 70 + 6580156606518226539973157608660353892749229031055061734000694135344872) * 10 ^ 70 + 8557530488504739440619376657922137403386809873696275093784855818108907) * 10 ^ 70 + 1303545078644921818696457139445144771662556255282934989528131022289810) * 10 ^ 70 + 4734884366136699353411052961763314055902251595303579194453102296412757
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_171 :
Polynomial.coeff recurrence4Scalar2Left 171 = -((((464459414 * 10 ^ 70 + 4389675184267077371446028501900242244017682715732326381392777464233685) * 10 ^ 70 + 2081444928684278462002296496458956826051764017936054346246509424074807) * 10 ^ 70 + 910517109651311099785668201165638194663725054600510857109857672661712) * 10 ^ 70 + 5848964243448120238754276464607287945973280864792910291902995674382603)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_172 :
Polynomial.coeff recurrence4Scalar2Left 172 = (((1418290084 * 10 ^ 70 + 5045119954465286382776794275182864393768115586163054331758133054400568) * 10 ^ 70 + 9073092756869077177994795597438058113197319338095919562799315292226336) * 10 ^ 70 + 4378271241806574336327538672508589556942641159959916133453277616052684) * 10 ^ 70 + 2259991371909429822401346665789932395710544221451698834252190719620186
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_173 :
Polynomial.coeff recurrence4Scalar2Left 173 = -((((4265817808 * 10 ^ 70 + 7861658944269470689717044064153186832376743397390939019195469979017411) * 10 ^ 70 + 2322942797387734740025640077159359452218264017422320510888427430932378) * 10 ^ 70 + 9881929543551724821670573283397301072494315444832519245422068245474421) * 10 ^ 70 + 4811794669302902601764198772709889965333139642165648851343277046002336)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_174 :
Polynomial.coeff recurrence4Scalar2Left 174 = (((12638139755 * 10 ^ 70 + 4891487460306863203374125591631231424844721896187962189224796825614835) * 10 ^ 70 + 3036780705436949170974937829305223776238317035877651518356165121993830) * 10 ^ 70 + 4265452158159563896936201420894092054985585193784370643929539099838715) * 10 ^ 70 + 3915114805249258960146642571907754286024465875171049127882703114778418
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_175 :
Polynomial.coeff recurrence4Scalar2Left 175 = -((((36883364205 * 10 ^ 70 + 390433235303856281258687416133616572545066882472671696203698441027996) * 10 ^ 70 + 5297062551799263627588027054417982367900133631354267694048042972921633) * 10 ^ 70 + 4710694620342573851233689704133663093953219348093871985961927875437341) * 10 ^ 70 + 6691280554381555406687744235325689987280360686337147601155430488840023)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_176 :
Polynomial.coeff recurrence4Scalar2Left 176 = (((106039233308 * 10 ^ 70 + 1801668450727077561988696852355267887104833623965802319495337016859090) * 10 ^ 70 + 7111070317188100088697194441095669209579071518257125512804709675706869) * 10 ^ 70 + 3482734541723016090375445498806640684307508244516521365706425940379028) * 10 ^ 70 + 6161616286153261867300678769296507999142892742654497394554111452327276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_177 :
Polynomial.coeff recurrence4Scalar2Left 177 = -((((300339687288 * 10 ^ 70 + 3100339352170976638508068687216349541696347222792884485541119168961188) * 10 ^ 70 + 145568120655604782876186227927208996502906001137898753783529530787907) * 10 ^ 70 + 7218434908546727687134697183007460696568315579826254944497905810565126) * 10 ^ 70 + 2103294547369496449143137557201101671643396340084209955537399528654924)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_178 :
Polynomial.coeff recurrence4Scalar2Left 178 = (((838088049676 * 10 ^ 70 + 6960653288051829836131858913333293030377420738761668145511081798128514) * 10 ^ 70 + 711799290094133858468868696036707070332026979597837851423193168242981) * 10 ^ 70 + 3076432658167346224408185545614955676823977693074501360011856163660050) * 10 ^ 70 + 9510371267277561083974752712146868865906534602997869971219615713709969
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_179 :
Polynomial.coeff recurrence4Scalar2Left 179 = -((((2304184850638 * 10 ^ 70 + 7388114614755980921931413542257494806559478893247667196733234468863080) * 10 ^ 70 + 9788192883041710299504862318108060540352132697521591040009401555285536) * 10 ^ 70 + 855801327759580369341459566694568411695927729897181695222281478761506) * 10 ^ 70 + 787135835419223462612650313774033578062948107421734295039552704341288)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_180 :
Polynomial.coeff recurrence4Scalar2Left 180 = (((6241873863135 * 10 ^ 70 + 9695772020518217520477363069605463605358848808820431158601627958573561) * 10 ^ 70 + 8849778729440670430186887126821175462065325152110471472776135631688361) * 10 ^ 70 + 1188619899451302420765205018511658409106865852852690196607270639315013) * 10 ^ 70 + 8072858534861610054337153746553914030687475527120794646000876818269182
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_181 :
Polynomial.coeff recurrence4Scalar2Left 181 = -((((16661005925268 * 10 ^ 70 + 4604274931627971881616356252655308213165927115704022996609031935619698) * 10 ^ 70 + 9268998075959981799574916633320096485561364517353994078064108684286680) * 10 ^ 70 + 8661407386244453607229925611757650292520306188728528994565291083555823) * 10 ^ 70 + 7708160014198739145086602440312793034404451911480395687415494199012256)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_182 :
Polynomial.coeff recurrence4Scalar2Left 182 = (((43822169501249 * 10 ^ 70 + 6256594626385258820181063357266558411674925552916176733195131343712045) * 10 ^ 70 + 2027679663671228470181405120017841275853639560382547514526418520646667) * 10 ^ 70 + 8054518236155759028703645603483188930305465719314483944509421972241609) * 10 ^ 70 + 2224288855143786750316762160213854610558715248060818779281791455980209
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_183 :
Polynomial.coeff recurrence4Scalar2Left 183 = -((((113582163107219 * 10 ^ 70 + 6968318931007580075409845081028362909808622491401416524519307359478521) * 10 ^ 70 + 2857414989371466189892691148836432370281065621032527798885408739817351) * 10 ^ 70 + 6206284052951645967225186172411336506885197589073400696656236526557026) * 10 ^ 70 + 9663241426287184915625374552259729791047717824294584819444405161416462)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_184 :
Polynomial.coeff recurrence4Scalar2Left 184 = (((290112541929000 * 10 ^ 70 + 1543863206339278677678707446991841973724709619119354897233934666905700) * 10 ^ 70 + 5040359546187365539718570981123616930996753145043674383615610869919526) * 10 ^ 70 + 1189415434107932220921849846658759063582724973101925075583516572863071) * 10 ^ 70 + 277292996316434749760861674104817651780320271461075406203356277408418
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_185 :
Polynomial.coeff recurrence4Scalar2Left 185 = -((((730262183491797 * 10 ^ 70 + 5420317713874676626918747180008920400358003301673159836773180740244247) * 10 ^ 70 + 1646836608805191966982049864578006740049875605171353406607771450636183) * 10 ^ 70 + 9419105937685423012873043075377991018976671977990555244334391333212707) * 10 ^ 70 + 9242453767295567069628404988185435502403110043379072835881482689176379)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_186 :
Polynomial.coeff recurrence4Scalar2Left 186 = (((1811599610756624 * 10 ^ 70 + 3882171581438688885367518253217136046453786494936763194968072070407520) * 10 ^ 70 + 7299658035227502181547000497698829283107947588719371015138720217671424) * 10 ^ 70 + 5810784102380175070901969748704096542847266765902117776179899890217692) * 10 ^ 70 + 8620088429151773409024817095009625239080926800767186232838386161855346
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_187 :
Polynomial.coeff recurrence4Scalar2Left 187 = -((((4429260511314907 * 10 ^ 70 + 3921888613912083922424766584194996615695987052191236320130256566323704) * 10 ^ 70 + 336807653056114540754290564926777655752585129855835943022903966896688) * 10 ^ 70 + 411025301312997626863343134962743617003222660233725058942581728569075) * 10 ^ 70 + 261123922245601714219819998995336883008497095597574655737917694700890)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_188 :
Polynomial.coeff recurrence4Scalar2Left 188 = (((10673323324514664 * 10 ^ 70 + 9610320197350452788636172938731884927068565489793556485266021651055176) * 10 ^ 70 + 1582562317606527943335976575717088452497030535637384025111409360120614) * 10 ^ 70 + 739097736945505084820822470595583031846012412316838905514300699693504) * 10 ^ 70 + 170154974095162202535692386421715635545083895759249896092184630863339
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_189 :
Polynomial.coeff recurrence4Scalar2Left 189 = -((((25350160852196087 * 10 ^ 70 + 1175471276862741672146065555412335337243872234753900363289743343360475) * 10 ^ 70 + 1691386667786483543984857539811165697146385309394785810795913975332169) * 10 ^ 70 + 7478831977385463463302413291112159449184687348888172616038629820584602) * 10 ^ 70 + 9857020984421708939523874081058281974563280016596053922481528862112033)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_190 :
Polynomial.coeff recurrence4Scalar2Left 190 = (((59345378524754538 * 10 ^ 70 + 5606142198742005212797115135372066813434754864499777654328954422143473) * 10 ^ 70 + 2716102936826538909947267332163696707203825579498305819706109068137048) * 10 ^ 70 + 4420642310755533355478390958681936282214159251131261989536162352116292) * 10 ^ 70 + 7753650833276428614431044328439948584805522376758021696808102411285848
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_191 :
Polynomial.coeff recurrence4Scalar2Left 191 = -((((136939923055145526 * 10 ^ 70 + 2427692991583306979876123138929150451947044068690014097884678271148321) * 10 ^ 70 + 5183856625259795973967021719703809633049740615999640927688765435398187) * 10 ^ 70 + 8374125303176151856308955067697039697029478519958463215613695068991172) * 10 ^ 70 + 872718775039336723257124261629579685821417028050224232777124481802593)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_192 :
Polynomial.coeff recurrence4Scalar2Left 192 = (((311473744170595156 * 10 ^ 70 + 2688427816357906881628829527928040328908455859659116313678960021207790) * 10 ^ 70 + 2745242107722619691211596899629775694245847165812008374664757313265306) * 10 ^ 70 + 816918767561123387791252722000996679621026865497462150434304396523837) * 10 ^ 70 + 2730671902797236474261024455054137278346759013301490688248281665170415
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_193 :
Polynomial.coeff recurrence4Scalar2Left 193 = -((((698347416559014457 * 10 ^ 70 + 6375930517575573132893181621394399231800639934895937633869318407243289) * 10 ^ 70 + 9978750165558514306698264511819436507573391232049770761289171824478963) * 10 ^ 70 + 9525503259912752602810007380759332306418510691810066251204815299283682) * 10 ^ 70 + 3016928882408511721663151492150021059062551537677296669797529328337172)