Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2ShiftPart1.Coefficients338To379

Recurrence 2 lookup certificate: Scalar2Shift coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_338 :
Polynomial.coeff recurrence2Scalar2Shift 338 = -((5778786031055 * 10 ^ 70 + 2335687071286094486961663076555375787175330782941148407483544434098996) * 10 ^ 70 + 5273810871066513466232116400358791003544943950261789762254746642075197)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_339 :
Polynomial.coeff recurrence2Scalar2Shift 339 = (198673512367 * 10 ^ 70 + 1077689650285588964614482296738935022722479095535754973004835187885711) * 10 ^ 70 + 2340695314270316521260679222910893419723850404160078216380484809997686
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_340 :
Polynomial.coeff recurrence2Scalar2Shift 340 = -((2426635354 * 10 ^ 70 + 6563436944277708324132343996993699191321277464239235909718299423927665) * 10 ^ 70 + 7511489069832839830145747258294401103694370141183421136124051713030155)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_341 :
Polynomial.coeff recurrence2Scalar2Shift 341 = -((28389610 * 10 ^ 70 + 9025214977511055237606527127340279099163680348027987799100490965834281) * 10 ^ 70 + 7886218089847867488394348304745335789678333043641446062007304485546755)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_342 :
Polynomial.coeff recurrence2Scalar2Shift 342 = (1352471 * 10 ^ 70 + 2332062430782527680433354862627482926733788477785140579386434090659608) * 10 ^ 70 + 9549872095294541799779993992469157563078973727312082535016960041897461
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_343 :
Polynomial.coeff recurrence2Scalar2Shift 343 = -((13977 * 10 ^ 70 + 4661209390748484090511382268732777924736338734666598222556910888511116) * 10 ^ 70 + 1796656032332666209674625258871452832042332029130842470335661038336611)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_344 :
Polynomial.coeff recurrence2Scalar2Shift 344 = -((83 * 10 ^ 70 + 3963007973445647394684802868540561777195674272148845292374426526779394) * 10 ^ 70 + 8589201925685753303004058481637921907619735234748901321452020709701604)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_345 :
Polynomial.coeff recurrence2Scalar2Shift 345 = (2 * 10 ^ 70 + 7658723067520799003264735789928602753875477731574051065293387444972044) * 10 ^ 70 + 2733102632544597222914205310123416038807758540976419243304376011578891
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_346 :
Polynomial.coeff recurrence2Scalar2Shift 346 = -(104556923824198389197223672247681097578920536715784198335562232850617 * 10 ^ 70 + 2733162134986152752944552209251921601480579497558719092785196254136564)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_347 :
Polynomial.coeff recurrence2Scalar2Shift 347 = -(1773065701499771117282861667572733360367736915290598846513713556738 * 10 ^ 70 + 6991455763697212834257259083349573116540458797671488071196448767203649)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_348 :
Polynomial.coeff recurrence2Scalar2Shift 348 = 13883616697406172259149793168734082563697578679239142889823589802 * 10 ^ 70 + 8723486323890445625824786090064489184972918477483956899135020551026786
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_349 :
Polynomial.coeff recurrence2Scalar2Shift 349 = 48637901797724479647081716574618131718667183019782447289440313 * 10 ^ 70 + 609461265111850276425698306553536315036995486831559210584343868978770
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_350 :
Polynomial.coeff recurrence2Scalar2Shift 350 = -(663587699540309659411128101367960197878841566351339071298078 * 10 ^ 70 + 5375596872786672431686631619627272107793808787569531471794618341846905)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_351 :
Polynomial.coeff recurrence2Scalar2Shift 351 = -(295104117160331000655067078740751632594048344301302673594 * 10 ^ 70 + 6136493055204515830988002993112191670135241962032001192004479014990201)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_352 :
Polynomial.coeff recurrence2Scalar2Shift 352 = 16552293616994860898276104118920731878641519155764719737 * 10 ^ 70 + 9644423227427761642468478653589608620621175246561613005876739952764098
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_353 :
Polynomial.coeff recurrence2Scalar2Shift 353 = -(16437273075595903160937542975402694738636658071103770 * 10 ^ 70 + 6856389201279867494525506038263382615913870144405965993124243865151160)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_354 :
Polynomial.coeff recurrence2Scalar2Shift 354 = -(226556500277038000492229348408799591477301397050391 * 10 ^ 70 + 6834349952019541430892757367058266973148162025058637122348847514667572)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_355 :
Polynomial.coeff recurrence2Scalar2Shift 355 = 461614717978296496022578514876381953460105916696 * 10 ^ 70 + 3130482444491374148937527488617864345656836046705338922027578620011790
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_356 :
Polynomial.coeff recurrence2Scalar2Shift 356 = 1535646552129404526727560724551810138890634433 * 10 ^ 70 + 8750874175168757165143429344607042162791942661995270779939945695082900
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_357 :
Polynomial.coeff recurrence2Scalar2Shift 357 = -(5139850723875795629331451755637974084483401 * 10 ^ 70 + 8352563594444732830265615595930204202766840376329462164246038138631201)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_358 :
Polynomial.coeff recurrence2Scalar2Shift 358 = -(2313702845568565530415398987431232892493 * 10 ^ 70 + 7728700059381116685251321798622926388693622892121183168924045086833539)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_359 :
Polynomial.coeff recurrence2Scalar2Shift 359 = 24627294337240439637338081448985985812 * 10 ^ 70 + 1126948231690071024957436647925151387730394745376886905562163062049882
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_360 :
Polynomial.coeff recurrence2Scalar2Shift 360 = -(23098802881734089736756213522286287 * 10 ^ 70 + 7289779074218179321893469342500389930167713340689369742885168940296003)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_361 :
Polynomial.coeff recurrence2Scalar2Shift 361 = -(27412882424994836981216441344195 * 10 ^ 70 + 987391626341116739434822587701329107935238162299255092856851501069094)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_362 :
Polynomial.coeff recurrence2Scalar2Shift 362 = 66381187252545886914105714805 * 10 ^ 70 + 8839851901313131558780029244944991649076579413174102705124069021886649
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_363 :
Polynomial.coeff recurrence2Scalar2Shift 363 = -(42269920347035084466766204 * 10 ^ 70 + 9505610790435517101310508923741488999289164359805252878270845883747506)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_364 :
Polynomial.coeff recurrence2Scalar2Shift 364 = 1441878404944981873787 * 10 ^ 70 + 7868839393847877829633575889587564781950971090812093617448482981553356
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_365 :
Polynomial.coeff recurrence2Scalar2Shift 365 = 9378695081447625320 * 10 ^ 70 + 2080155126996890273893904604449552343087024251166309094594484759471213
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_366 :
Polynomial.coeff recurrence2Scalar2Shift 366 = -(3907193356887333 * 10 ^ 70 + 3836043868019426240340717492647342362803543124882775221109984303318960)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_367 :
Polynomial.coeff recurrence2Scalar2Shift 367 = 561997906271 * 10 ^ 70 + 5494429701032508268890386466862784877464913594422174070297961782685286
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_368 :
Polynomial.coeff recurrence2Scalar2Shift 368 = -(14572594 * 10 ^ 70 + 3894983591051645115314716535612074173183188716354308215725481462148398)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_369 :
Polynomial.coeff recurrence2Scalar2Shift 369 = -(2739 * 10 ^ 70 + 3570940864937326967300021910482763294962810303007411004902032802076913)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_370 :
Polynomial.coeff recurrence2Scalar2Shift 370 = 1910243966047913114248399737805887557802228692164026247523475754151739
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_371 :
Polynomial.coeff recurrence2Scalar2Shift 371 = -36917311953252292795537222966523524068792196790010526163665254815
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_372 :
Polynomial.coeff recurrence2Scalar2Shift 372 = 183363243886378695115034101466851023187338729371592055258833
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_373 :
Polynomial.coeff recurrence2Scalar2Shift 373 = 325625577524957324677044466501864311979116908083955817
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_374 :
Polynomial.coeff recurrence2Scalar2Shift 374 = -2079834844921096051394689788341353856730288452634
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_375 :
Polynomial.coeff recurrence2Scalar2Shift 375 = 1518996951250413818027197278673846063992040
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_376 :
Polynomial.coeff recurrence2Scalar2Shift 376 = -127251674289765160684473866441357158
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_377 :
Polynomial.coeff recurrence2Scalar2Shift 377 = 671580179972517182291550039
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_378 :
Polynomial.coeff recurrence2Scalar2Shift 378 = 981405724590120839
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_379 :
Polynomial.coeff recurrence2Scalar2Shift 379 = -656766259