Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1ExceptionalPart1.Coefficients232To257

Recurrence 2 lookup certificate: Scalar1Exceptional 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.recurrence2Scalar1Exceptional_coeff_232 :

Polynomial.coeff recurrence2Scalar1Exceptional 232 = -((2819676551946552444506912537609423547150890319177181303314499 * 10 ^ 70 + 7490511606212597674445757825789441873843294463199613021386539462165854) * 10 ^ 70 + 7026992915505631166236413929382579951535624864845277908725257631369477)

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

Polynomial.coeff recurrence2Scalar1Exceptional 233 = (1432276624385986062281391637082896463649105686991472412733498 * 10 ^ 70 + 2265290247187417628242043324349532303876888571492415295262794276951156) * 10 ^ 70 + 4384986900630767649896018697331298473792471231568268490368779879458652

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

Polynomial.coeff recurrence2Scalar1Exceptional 234 = -((477741232011220236137254494498605760915692906873648885909119 * 10 ^ 70 + 5354255850162012068531848478298369230209919879581884703558882513008835) * 10 ^ 70 + 7920347111404188133263746005588375897342563499624841499289318602353294)

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

Polynomial.coeff recurrence2Scalar1Exceptional 235 = -((87418179139672334821163987532148395052136985499837576136036 * 10 ^ 70 + 785415221425189954987415428806050927049346985107828713616513397742933) * 10 ^ 70 + 1077176111619049513424998633897408136805254838771613329363949605750906)

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

Polynomial.coeff recurrence2Scalar1Exceptional 236 = (351936079271248822834416774726641438086919652572902324497429 * 10 ^ 70 + 9921615997115107878607837082650421012238941374892413883755570159433148) * 10 ^ 70 + 4947551586700919820395903253508536691665310130226470250393828063734806

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

Polynomial.coeff recurrence2Scalar1Exceptional 237 = -((416309087917443952772700458743103287415201498588745427597573 * 10 ^ 70 + 9518421468219433566517329396438522729928160505729656816320887997321484) * 10 ^ 70 + 6535715380542595880281687604390369570318643027009143529372764459687517)

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

Polynomial.coeff recurrence2Scalar1Exceptional 238 = (369715207999975687498979985109243068089424614581498428174460 * 10 ^ 70 + 9096753480169543424805328095093749071858026259773916419719699882353199) * 10 ^ 70 + 2175733374225227766653285278501942007761262404883994819636398595064653

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

Polynomial.coeff recurrence2Scalar1Exceptional 239 = -((278488622545293041585956257717105123669710164344918355789287 * 10 ^ 70 + 579117797173720697124596098419751249244317491826186051861614503954640) * 10 ^ 70 + 3415793139080419906068761966013590302488278982660868535651296656974465)

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

Polynomial.coeff recurrence2Scalar1Exceptional 240 = (184084471734795101265493975845217240683963325484680132074180 * 10 ^ 70 + 3430987247856752924692820142212651077396300612372221881245864209183818) * 10 ^ 70 + 5551264154907612316201480787991101887194626899126781956694122089227767

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

Polynomial.coeff recurrence2Scalar1Exceptional 241 = -((107014225502080179636611711874877609523498405490472999938996 * 10 ^ 70 + 3553305486851845009096566858476731385119412907208020869912308405574818) * 10 ^ 70 + 9439324373919284268514281640627674080060292108940227504484401575790256)

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

Polynomial.coeff recurrence2Scalar1Exceptional 242 = (53268185196709875495452288915761832097337805311495263964292 * 10 ^ 70 + 1161050788520305844149725023813727700083013937082465350661692490217968) * 10 ^ 70 + 2530142997682019929787006729718061011917881087204002121572541722132256

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

Polynomial.coeff recurrence2Scalar1Exceptional 243 = -((20660056278695368389468310511269569031714177928499665738086 * 10 ^ 70 + 4753802909284420807975330062465340508148467742955475815041856113856823) * 10 ^ 70 + 1400290459961186648146239529187372345409707310629916578748178677775273)

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

Polynomial.coeff recurrence2Scalar1Exceptional 244 = (3708159911845495838816237309724040300844466724013042876722 * 10 ^ 70 + 8152425902776604195877784521268490661057963604552874911789212130465797) * 10 ^ 70 + 653948371685656335674186470120711977391319167272864523974523754775250

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

Polynomial.coeff recurrence2Scalar1Exceptional 245 = (3328376962734195713699421396102434210958414027434285068066 * 10 ^ 70 + 3516010065905445243175911858116551299832966025371360299496889707243944) * 10 ^ 70 + 5001233097825034638054935720817036170425533901203008315102173782586202

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

Polynomial.coeff recurrence2Scalar1Exceptional 246 = -((5007804572655512127706116469295513999163874561734253949577 * 10 ^ 70 + 1200753101189116943552425352445735195417422726173227400532549583130861) * 10 ^ 70 + 8308805093454173124332575102832268939386157297071088146770217006274575)

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

Polynomial.coeff recurrence2Scalar1Exceptional 247 = (4346347368262344260777223311786838568611869001920285587692 * 10 ^ 70 + 1328401304316570731488596731453992406833100689141244697526040535457477) * 10 ^ 70 + 4877258226999847288013456929113742144989731420507915122123137583139835

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

Polynomial.coeff recurrence2Scalar1Exceptional 248 = -((3031252339152936054336626804351560160619454176111189395601 * 10 ^ 70 + 6418518796861323337884160261718603128677431028357300130859158154747301) * 10 ^ 70 + 622103321613377866752752153421551732864654405583257546034233406228012)

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

Polynomial.coeff recurrence2Scalar1Exceptional 249 = (1829737328646886324775127180859485432066894761225256999765 * 10 ^ 70 + 3670190097113724381368412810454183860548473702964978854281729921185119) * 10 ^ 70 + 5431776367233419001100260077171459891072202033834182528848449896632753

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

Polynomial.coeff recurrence2Scalar1Exceptional 250 = -((977885252668880725436570755142890284065292110253008967170 * 10 ^ 70 + 8500381122958995750147135078013032359275127856533456649477279647313104) * 10 ^ 70 + 9460264577230239099113143167007554782238363847791828946135079973424786)

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

Polynomial.coeff recurrence2Scalar1Exceptional 251 = (462680360884226765640746469540146874321768206725339253728 * 10 ^ 70 + 1837778021661307189484853443745130044820629298225307071423050546841135) * 10 ^ 70 + 70459615434331029709488107305170923328342317726112122557711556920285

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

Polynomial.coeff recurrence2Scalar1Exceptional 252 = -((189509384473009835231598959079818495461256117048099092420 * 10 ^ 70 + 3386175754733496934020236430008738183800272415098429080223994709465310) * 10 ^ 70 + 9750793973255415586009522695990790485947350414493240087842751686699659)

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

Polynomial.coeff recurrence2Scalar1Exceptional 253 = (62578288740950193304043249076179533716631859279760704349 * 10 ^ 70 + 6419307912672807765295089043511572484100592582722501083428440360442590) * 10 ^ 70 + 2601136686714331377958549197387784481714816241107825781289153890491454

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

Polynomial.coeff recurrence2Scalar1Exceptional 254 = -((12309122191429791566802166343085508415604967172156251265 * 10 ^ 70 + 5380516539234476833196302516645916358133368203736715712881178756782193) * 10 ^ 70 + 3758910923809110548890083578542767801717394124008932783144152327137782)

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

Polynomial.coeff recurrence2Scalar1Exceptional 255 = -((3140921342407701941516646224934551349633883329919610407 * 10 ^ 70 + 8770039180183140913385188887944037918110522935872758580408738527633834) * 10 ^ 70 + 4744852152717786989988945382484785642027395293483961731981671944579131)

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

Polynomial.coeff recurrence2Scalar1Exceptional 256 = (5368192546869991016298689728417833375746531738950104112 * 10 ^ 70 + 7764800419039775375585162008944193617255533584449105076929056631377310) * 10 ^ 70 + 811444353028877725185217394329425456476634425224758264516582766267977

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

Polynomial.coeff recurrence2Scalar1Exceptional 257 = -((3905159181408071521159545545392852530707606860569942963 * 10 ^ 70 + 1662744717549905767370524122106174952892764885511679298199198645842996) * 10 ^ 70 + 1773169420983773883957236325964725193459557609262723140352093348668579)