Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC1Low.Coefficients25To48

Recurrence 2 lookup certificate: C1 source coefficients, low half #

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.recurrence2C1_coeff_25 :
Polynomial.coeff remainder4Coefficient1 25 = -2440782889814689114143345791756460874707886213473249228266
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_26 :
Polynomial.coeff remainder4Coefficient1 26 = 71611976960909361709623286107178577864223922136607516429486
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_27 :
Polynomial.coeff remainder4Coefficient1 27 = -1910893655236790414036807360120439706498056222349982999372260
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_28 :
Polynomial.coeff remainder4Coefficient1 28 = 46544511128236073210085191888112542851680838041596196178995233
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_29 :
Polynomial.coeff remainder4Coefficient1 29 = -1038382401547817885136538493771201872301813264476381906664283005
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_30 :
Polynomial.coeff remainder4Coefficient1 30 = 21285255821139194749000870147779267836589650298476565440425515592
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_31 :
Polynomial.coeff remainder4Coefficient1 31 = -402085487617173171346990294959042376926569851681638036112426825704
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_32 :
Polynomial.coeff remainder4Coefficient1 32 = 7019056457487341598636866118648688426911261501437102308811044247647
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_33 :
Polynomial.coeff remainder4Coefficient1 33 = -113523928149350087463274312433599322256128549853878190619109597165150
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_34 :
Polynomial.coeff remainder4Coefficient1 34 = 1705308121530463853100420746914649885839122515704567802777551156880432
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_35 :
Polynomial.coeff remainder4Coefficient1 35 = -(2 * 10 ^ 70 + 3846242155032942185219835867887039027276005848195794060774553771719276)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_36 :
Polynomial.coeff remainder4Coefficient1 36 = 31 * 10 ^ 70 + 1081990263117924439353141722672607209777681404731533157872778141782439
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_37 :
Polynomial.coeff remainder4Coefficient1 37 = -(379 * 10 ^ 70 + 3582370910840075862409938468717334008044243103250093032519498845893707)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_38 :
Polynomial.coeff remainder4Coefficient1 38 = 4332 * 10 ^ 70 + 8679102116464914644499967959765679694413608273947868630111004415558231
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_39 :
Polynomial.coeff remainder4Coefficient1 39 = -(46434 * 10 ^ 70 + 1412824802207795165982896394565698905327169863766004237044652872787051)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_40 :
Polynomial.coeff remainder4Coefficient1 40 = 467709 * 10 ^ 70 + 9489640300693453277827296233261471078251682098182814108216217126233074
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_41 :
Polynomial.coeff remainder4Coefficient1 41 = -(4434999 * 10 ^ 70 + 3169001452735916826949746261266378307625072208658338631430722105224758)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_42 :
Polynomial.coeff remainder4Coefficient1 42 = 39650697 * 10 ^ 70 + 4715509006355921014001756983287399272159843432897646526140258307256269
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_43 :
Polynomial.coeff remainder4Coefficient1 43 = -(334715223 * 10 ^ 70 + 1218939706398567819690138921574942427585452799742893316378194253424408)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_44 :
Polynomial.coeff remainder4Coefficient1 44 = 2671537060 * 10 ^ 70 + 2051296174841611855241922811619513307918884962763545869732363137094506
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_45 :
Polynomial.coeff remainder4Coefficient1 45 = -(20186943079 * 10 ^ 70 + 592368397514798445235365221231949766144764030429083619970355494260923)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_46 :
Polynomial.coeff remainder4Coefficient1 46 = 144589483213 * 10 ^ 70 + 8634850830470801259681251655578745859131861940650802324456658941038276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_47 :
Polynomial.coeff remainder4Coefficient1 47 = -(982800184742 * 10 ^ 70 + 4781282784301230391310291474605166532410612621780784206841688976628421)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C1_coeff_48 :
Polynomial.coeff remainder4Coefficient1 48 = 6346521276594 * 10 ^ 70 + 5515894754749045243451932014894939781253382315596239544403847447594929