Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupB2A4Part1.Coefficients246To276

Recurrence 4 lookup certificate: B2A4 coefficient convolution #

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_246 :

Polynomial.coeff recurrence4B2A4 246 = (1022636300822137409318573662489725618761610064 * 10 ^ 70 + 4983809373632550546348979380417819516091513025098443861856418289698787) * 10 ^ 70 + 9349230086244777498040140977422650692158022824033930674704948010224215

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_247 :

Polynomial.coeff recurrence4B2A4 247 = -((520590591650682011788549336345715065318374020 * 10 ^ 70 + 932437153474331064338905710236923984156330347803198138692057544980775) * 10 ^ 70 + 3395086018251390178499572914410100231078201890431945797219192125574039)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_248 :

Polynomial.coeff recurrence4B2A4 248 = (247884709027763749552822530119983402540236766 * 10 ^ 70 + 3214251855898288864718228756903298117940364998727921588028723600960144) * 10 ^ 70 + 566923716846565065669777982258115277249908754264825251497046044588488

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_249 :

Polynomial.coeff recurrence4B2A4 249 = -((112252098445660785857174333623376269471426503 * 10 ^ 70 + 6144885975284816647091985662061337388952954028285085988718928512443041) * 10 ^ 70 + 7260162531958260750749595518390265999494049470140810670204994978303263)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_250 :

Polynomial.coeff recurrence4B2A4 250 = (48717338058998127084421328502049622121654789 * 10 ^ 70 + 6345710101253439111586479196199128342611004008400089842126554493625606) * 10 ^ 70 + 2522026653916509184588961382037672732625965632574738732297170239850986

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_251 :

Polynomial.coeff recurrence4B2A4 251 = -((20331783392667689324414413107743024703033017 * 10 ^ 70 + 5392168289974746717131332802646744972888774808624236014712715398236928) * 10 ^ 70 + 3685934898833216155990438989945825082543361825847723109084790460041504)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_252 :

Polynomial.coeff recurrence4B2A4 252 = (8166920074885272137192707277612534405133700 * 10 ^ 70 + 9768108434185049589976683825094756190875797195983313189085072986241205) * 10 ^ 70 + 9529668864002702862192605677778963506222298206602044995407868488344173

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_253 :

Polynomial.coeff recurrence4B2A4 253 = -((3155131110350471156517864434452338826315315 * 10 ^ 70 + 3301253855302085345805437604205296229726583737312743245054573405406802) * 10 ^ 70 + 1742207207218258216333787847400287414784965130311038585758591796193265)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_254 :

Polynomial.coeff recurrence4B2A4 254 = (1169975868935888988211850063555807890423003 * 10 ^ 70 + 199783997294183622075644929038070186945882876447063367125493049995388) * 10 ^ 70 + 1777057162215959961013632834875795065455243916285994673050913548458990

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_255 :

Polynomial.coeff recurrence4B2A4 255 = -((415042752812289781086058489435137072806275 * 10 ^ 70 + 9429563176392617414040568189016109813069810096833277864734066312184724) * 10 ^ 70 + 1392389958166063989320144805241457075196584312761731186506659051434230)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_256 :

Polynomial.coeff recurrence4B2A4 256 = (140152562309146105263806519398432155098669 * 10 ^ 70 + 8402131537624330324629895156161063031227666461947652034057399166928934) * 10 ^ 70 + 7837527683465360467535315023928804103039510192122542711294224918697227

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_257 :

Polynomial.coeff recurrence4B2A4 257 = -((44714358550152538840981032070835779135088 * 10 ^ 70 + 3091012665889998700866809190781519622878939056646181876959740733840426) * 10 ^ 70 + 1898781903760044983657470000657401513310333752641660858962105880650783)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_258 :

Polynomial.coeff recurrence4B2A4 258 = (13318978432944377299039994468663903214729 * 10 ^ 70 + 783739195005546510240971628319928677963100986672501809188393146318808) * 10 ^ 70 + 9414294183022395252736632224591259887214610781889882243101700435530223

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_259 :

Polynomial.coeff recurrence4B2A4 259 = -((3627939608531022452148827983692843740122 * 10 ^ 70 + 4595377663141181159707277861995795086375417007255544395127323243398346) * 10 ^ 70 + 6100737436932501207814951634254820564288983502790462290805321254224442)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_260 :

Polynomial.coeff recurrence4B2A4 260 = (866061667704277467368178799699627628307 * 10 ^ 70 + 2160461800103124839604358831714263728417413620108300933161563742659408) * 10 ^ 70 + 4304425235627822912642103332723952611461825920901554682496717112063089

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_261 :

Polynomial.coeff recurrence4B2A4 261 = -((161286158111695095123304651776059594501 * 10 ^ 70 + 1784326692380633174501287899732501728303466052373994810688944832970098) * 10 ^ 70 + 2240369494894603845306351615066732249053749858443281160476430277537836)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_262 :

Polynomial.coeff recurrence4B2A4 262 = (11488212318236743515296274763572907778 * 10 ^ 70 + 2988632518601307619330915605374971256403379970938627459130102945065363) * 10 ^ 70 + 8557016028582277624442802547323661817614578568507301077794407291811834

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_263 :

Polynomial.coeff recurrence4B2A4 263 = (8706959373614717314802233169881832840 * 10 ^ 70 + 9611229569968006458216972269329843722898805898661496226981752948783384) * 10 ^ 70 + 7815416180251739436308589415838444629098454163398026740132465086620855

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_264 :

Polynomial.coeff recurrence4B2A4 264 = -((6172928788036532122476328645518304449 * 10 ^ 70 + 6508219907444786034868302924400433138817766746996129336605453424291613) * 10 ^ 70 + 4962150889717862319773152809893961026092073905991388537874255397123284)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_265 :

Polynomial.coeff recurrence4B2A4 265 = (2779478096919087517561491480239297524 * 10 ^ 70 + 8833963038844710144339124030443317729571956348740483675946504858166586) * 10 ^ 70 + 100829379055882576976098998390285513599878239037904869110531022965303

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_266 :

Polynomial.coeff recurrence4B2A4 266 = -((1048929080843772534055147414807387858 * 10 ^ 70 + 5900703097715895560529754141380601550126844612139372160939648911530170) * 10 ^ 70 + 4365157584433972108194514181774392026826781905968625838775070301500223)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_267 :

Polynomial.coeff recurrence4B2A4 267 = (361022768514372942967373218452714641 * 10 ^ 70 + 6742213481698359748935738165912837733152270271913979737240986055541437) * 10 ^ 70 + 896587070272657469377957700830579857016645677239710624888949006031206

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_268 :

Polynomial.coeff recurrence4B2A4 268 = -((119611217923065334287878663464936777 * 10 ^ 70 + 2764663428124341479305707706926587469500854804922784562321761559204548) * 10 ^ 70 + 6259483053661580489361024734383621092187086319725962128507351063233669)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_269 :

Polynomial.coeff recurrence4B2A4 269 = (40096233818016085309299606384676015 * 10 ^ 70 + 2297362028309761759587201722048929625082843378722877250622672549628971) * 10 ^ 70 + 517967484174023682932172657775263502077798917589565953145520997416153

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_270 :

Polynomial.coeff recurrence4B2A4 270 = -((14167810490793897420424205187566176 * 10 ^ 70 + 8709827763912880933336434281003327110775932650111325262113440978293161) * 10 ^ 70 + 1269525091897442643009283532004765139208936906602885874214109775494953)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_271 :

Polynomial.coeff recurrence4B2A4 271 = (5351135931574662746061280362766716 * 10 ^ 70 + 9493210813000900788386252203295430960525901062953105273314533243258794) * 10 ^ 70 + 5691676577880413565054360316770716165697529337725665440913696366843272

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_272 :

Polynomial.coeff recurrence4B2A4 272 = -((2122348227363119441197581860752171 * 10 ^ 70 + 6072035986904204514990015146669807984247275048789938590975400915638219) * 10 ^ 70 + 1582235527404516293018568231772178815968388954339039155712630259167830)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_273 :

Polynomial.coeff recurrence4B2A4 273 = (856292116773396210950883083466714 * 10 ^ 70 + 2504066838354820883504399586568688594448146681099521733203688374688789) * 10 ^ 70 + 4617537743470343740269969076838935691829890656137781475587657689055281

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_274 :

Polynomial.coeff recurrence4B2A4 274 = -((342041182759926694927373920494022 * 10 ^ 70 + 4951683205249891339720387078063237026661607858872650943856704480075586) * 10 ^ 70 + 4822977214253164853590788260888665219187857861583272359544995783125309)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_275 :

Polynomial.coeff recurrence4B2A4 275 = (132981673443574913628310132674163 * 10 ^ 70 + 6867482674880309392277874111314576568397670082091447125665257312352367) * 10 ^ 70 + 2938362217250775789987334851715534622187042843345897282587234710565131

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B2A4_coeff_276 :

Polynomial.coeff recurrence4B2A4 276 = -((49840764978779568967390930924058 * 10 ^ 70 + 810515060407324049231202436954625939858467301446187894031949377176718) * 10 ^ 70 + 1005522392667739972804238157724804279475568784263308147120625342406981)