Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2ExceptionalPart1.Coefficients257To284

Recurrence 2 lookup certificate: Scalar2Exceptional 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.recurrence2Scalar2Exceptional_coeff_257 :

Polynomial.coeff recurrence2Scalar2Exceptional 257 = -((439688309468970457290467341799760195914209488620361405 * 10 ^ 70 + 8228296278715177774010074940222824785751632167332530700096951422916580) * 10 ^ 70 + 3296610615662980405924855790257692289742979937134618903892841962500463)

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

Polynomial.coeff recurrence2Scalar2Exceptional 258 = (212793299342856833839053377369359954812545246831088850 * 10 ^ 70 + 6924320038775870228568318110051656928227913419959171000390938550458077) * 10 ^ 70 + 3973959554498507079704391899764656057231478408022155832792520558005351

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

Polynomial.coeff recurrence2Scalar2Exceptional 259 = -((89796650442966042492913222341599518012241420245548091 * 10 ^ 70 + 5891337298296137481289788308943370023565413723893320994988465211951526) * 10 ^ 70 + 5308220239643347198045810406962250625220096152104806920613216624424665)

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

Polynomial.coeff recurrence2Scalar2Exceptional 260 = (32670760570195642837953305445026011550662441711621570 * 10 ^ 70 + 7213651909317300319897475599737807550251067486617605511237075019542239) * 10 ^ 70 + 8301264490853517831359689119183250099958209677052371402933209048206923

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

Polynomial.coeff recurrence2Scalar2Exceptional 261 = -((9629091384981221792945180894991288782551293101037913 * 10 ^ 70 + 2549968104166771050195079462061790250553284878627191600018099768368131) * 10 ^ 70 + 2487901249822569919376615193560309337268698524007589423230398827760830)

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

Polynomial.coeff recurrence2Scalar2Exceptional 262 = (1750371422170842361714800837589581261180070468565533 * 10 ^ 70 + 6665688942068635049271586908729732158280272191767666350871710202061825) * 10 ^ 70 + 149781354541365110004574037680526764548743521297351703162580697703675

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

Polynomial.coeff recurrence2Scalar2Exceptional 263 = (311965556430972384890604735726328773865185986817609 * 10 ^ 70 + 141667749943978102712380711894594884241684442448906537732361093846613) * 10 ^ 70 + 28190238908208748308300553723012666054616223540613355544030274909734

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

Polynomial.coeff recurrence2Scalar2Exceptional 264 = -((530593836264933805365345827550430853322105393301232 * 10 ^ 70 + 9465433175806202156833823104690481772261808112947411650417158760516066) * 10 ^ 70 + 1842931897963653295628711522453311309777225810607293550021698974436453)

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

Polynomial.coeff recurrence2Scalar2Exceptional 265 = (344900487900388824079563653599170651304621552848195 * 10 ^ 70 + 4990805701451841201376692276877091939457849430951773547634545317289417) * 10 ^ 70 + 6174750003323999466618129246905499660870774526589479097109943718056766

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

Polynomial.coeff recurrence2Scalar2Exceptional 266 = -((168843619826711632991801451029881002578671303643594 * 10 ^ 70 + 4386899281386328292171139475308777512533033497316715531745830023903188) * 10 ^ 70 + 3986433291849433356826725922318979804419394895635028339190110053892290)

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

Polynomial.coeff recurrence2Scalar2Exceptional 267 = (68827501250110407117028171692860032756756823453333 * 10 ^ 70 + 1123763538547862227685443333701360152061694768266266893909211646796239) * 10 ^ 70 + 713083549240207410483667755423508443003796343996702042121345776943922

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

Polynomial.coeff recurrence2Scalar2Exceptional 268 = -((23897471023767231508586826957211613256505680049936 * 10 ^ 70 + 9721335523748634200613455940835276117301732243862806000163789052137638) * 10 ^ 70 + 7829393622651725514071199110499352037088848710743179732613579609276561)

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

Polynomial.coeff recurrence2Scalar2Exceptional 269 = (7038837491558450252619125080474731257040841336741 * 10 ^ 70 + 6676116419338913528571475630298854320046143680550903912528630850076874) * 10 ^ 70 + 9582412292501191161390194891102133710704534532436529146301104229707606

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

Polynomial.coeff recurrence2Scalar2Exceptional 270 = -((1746393425905647613515845202106618740503723736385 * 10 ^ 70 + 7009658367351753951477926860145834672901493435508128306786897176716077) * 10 ^ 70 + 2900417195389137122211906966004115437422826522508596767805569491363583)

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

Polynomial.coeff recurrence2Scalar2Exceptional 271 = (390944837008536232662200418259289054631123054882 * 10 ^ 70 + 1964530823471878737561806702046711609035510425537253479002112363635994) * 10 ^ 70 + 4938213873693654067990970762265683752355175574961785316913614116359750

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

Polynomial.coeff recurrence2Scalar2Exceptional 272 = -((113024002451601375880740502017451322805264006243 * 10 ^ 70 + 5549631949093500117094425653280102997951293754425492755380009118586804) * 10 ^ 70 + 4520822839009768323026951652118445336874033549833283145571774664914061)

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

Polynomial.coeff recurrence2Scalar2Exceptional 273 = (54578357646183583908814843173658143338836623820 * 10 ^ 70 + 875678996264384971548501836692291919528240646357217554455255570547747) * 10 ^ 70 + 9441764058022994076601200857197703723806320497807364593089102755493746

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

Polynomial.coeff recurrence2Scalar2Exceptional 274 = -((26945752836193164093020437500440587107554070550 * 10 ^ 70 + 726147044359837993376344538995050594119558947487657511596902012883421) * 10 ^ 70 + 7185059484763680282055191896947856342241866841598239309126333044616395)

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

Polynomial.coeff recurrence2Scalar2Exceptional 275 = (8125753056556697696286732239201468392565493961 * 10 ^ 70 + 4890535602100244361055489869159037775607425228510346612698022404880305) * 10 ^ 70 + 2696478741282741373582026389571176611607522054478956877284687168130861

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

Polynomial.coeff recurrence2Scalar2Exceptional 276 = (1414821526824699234413477378851705996946437498 * 10 ^ 70 + 3988847926998264904420812616455481670501936119731102472145530601453763) * 10 ^ 70 + 5740802343277538850478148785703489213456090085940751481834335761444350

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

Polynomial.coeff recurrence2Scalar2Exceptional 277 = -((4005897262975037512738367681893531637341087802 * 10 ^ 70 + 3666267877802618502940727959004250313795220565008300393179049743821181) * 10 ^ 70 + 2826913761681242856050004997389573274170639873691891856265055216087814)

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

Polynomial.coeff recurrence2Scalar2Exceptional 278 = (3345228176540276371804741579384905786910690115 * 10 ^ 70 + 8091770215939509636498199720113857805202134101819598454380679065760824) * 10 ^ 70 + 4815717875865776648617614977250162158204430337929611262469048394757410

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

Polynomial.coeff recurrence2Scalar2Exceptional 279 = -((1964953887887406427598277797666706172820992710 * 10 ^ 70 + 8603448283168380876555493127483902713906134660144075735188287850245442) * 10 ^ 70 + 7232176255467159379927605722526921179196815552226804679418289267752150)

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

Polynomial.coeff recurrence2Scalar2Exceptional 280 = (904438307255582041257839467120960677392282539 * 10 ^ 70 + 1655162185406202790618320526959502080258727125908627961350701376451943) * 10 ^ 70 + 7069199870127777124794384727291867460378772238143332330381476468786972

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

Polynomial.coeff recurrence2Scalar2Exceptional 281 = -((323895734877359746477971086231382821598918158 * 10 ^ 70 + 131457589661761409002917386012765671400736141817959961970710727587314) * 10 ^ 70 + 8056487936212359319372915938825842440510833476929630821169993542007058)

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

Polynomial.coeff recurrence2Scalar2Exceptional 282 = (77209092170927876593462980052832546108579289 * 10 ^ 70 + 900392085186915865007729425404645451442029103257006866454581131907521) * 10 ^ 70 + 4474027313445616442924790417107559667198055869223828574517423479421836

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

Polynomial.coeff recurrence2Scalar2Exceptional 283 = (1026043635217218094887550433735033242777295 * 10 ^ 70 + 5811836313511546457770352172072429058740824275184913988241240623813204) * 10 ^ 70 + 6364934251767483307813183255812898152639716433957143792664971511551465

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

Polynomial.coeff recurrence2Scalar2Exceptional 284 = -((14233189156523677521421212883005881549755041 * 10 ^ 70 + 5074034108029359172357253726307860658364889863922691084341291308018545) * 10 ^ 70 + 8651973453690273369461242749001231139922346466663166746689663254432381)