Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0LeftPart0.Coefficients0To40

Recurrence 4 lookup certificate: Scalar0Left coefficient convolution #

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

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_0 :
Polynomial.coeff recurrence4Scalar0Left 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_1 :
Polynomial.coeff recurrence4Scalar0Left 1 = -956033368688907243392302809638568532869120
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_2 :
Polynomial.coeff recurrence4Scalar0Left 2 = 2035939666856210925036617294642176608682192896
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_3 :
Polynomial.coeff recurrence4Scalar0Left 3 = 21162950099910863018132271059959809869575315353600
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_4 :
Polynomial.coeff recurrence4Scalar0Left 4 = -132290974344460475854466767936055460169212491505454848
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_5 :
Polynomial.coeff recurrence4Scalar0Left 5 = 350840852257233413802932470543512662399192681836079108352
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_6 :
Polynomial.coeff recurrence4Scalar0Left 6 = -540881519986109736505128043780595679960896334359076814770000
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_7 :
Polynomial.coeff recurrence4Scalar0Left 7 = 524983290515435684698342384717972549255836054710467167554359776
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_8 :
Polynomial.coeff recurrence4Scalar0Left 8 = -333524259082078755982462545762437962674345925659675531696185925252
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_9 :
Polynomial.coeff recurrence4Scalar0Left 9 = 151777817199192759287214497564225748840832069387794482193977366505132
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_10 :
Polynomial.coeff recurrence4Scalar0Left 10 = -(6 * 10 ^ 70 + 3789438510792076960782734964570318940419596928608868674638697912670040)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_11 :
Polynomial.coeff recurrence4Scalar0Left 11 = 2592 * 10 ^ 70 + 3167865687119761642664514784601965405424619836747514422743908793760124
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_12 :
Polynomial.coeff recurrence4Scalar0Left 12 = -(568923 * 10 ^ 70 + 1659608789426311409756512620529417252395361292148718427698406375340284)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_13 :
Polynomial.coeff recurrence4Scalar0Left 13 = -(202360450 * 10 ^ 70 + 7165551712562588561660997133327850925868150049692146174663792209665300)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_14 :
Polynomial.coeff recurrence4Scalar0Left 14 = 242965396393 * 10 ^ 70 + 1870840738803041745158510643530619584035315549282566530860646923054488
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_15 :
Polynomial.coeff recurrence4Scalar0Left 15 = -(123818725105637 * 10 ^ 70 + 1836213643208900308846640671667505322224185146058273913040947443180800)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_16 :
Polynomial.coeff recurrence4Scalar0Left 16 = 49654403603503748 * 10 ^ 70 + 6639550767040404652350944201738236930899183236575123267269417323319080
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_17 :
Polynomial.coeff recurrence4Scalar0Left 17 = -(18053053522028586943 * 10 ^ 70 + 3069629735590447067482767815719921956976229161076283549152031154322256)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_18 :
Polynomial.coeff recurrence4Scalar0Left 18 = 4981747561080371216148 * 10 ^ 70 + 107192382786951188043995135256494465960449098499746309522210144390347
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_19 :
Polynomial.coeff recurrence4Scalar0Left 19 = -(358983589670808836926496 * 10 ^ 70 + 4482974327494428523924939678169229001249598689372628397221483771902177)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_20 :
Polynomial.coeff recurrence4Scalar0Left 20 = -(517940007395599801627754419 * 10 ^ 70 + 8812688751161534451079640041451319179553215959363207736293405142954496)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_21 :
Polynomial.coeff recurrence4Scalar0Left 21 = 333436542743350296690626252187 * 10 ^ 70 + 2762936406697982388858516320402479269749626164023637817064415181599287
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_22 :
Polynomial.coeff recurrence4Scalar0Left 22 = -(118380423911552037331777863563626 * 10 ^ 70 + 7366003131222934670919448671173408360037866138533459590830770527416120)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_23 :
Polynomial.coeff recurrence4Scalar0Left 23 = 28541749487957886905182207116071974 * 10 ^ 70 + 5971678299132564895549215348107910257587985217095350427445536189928851
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_24 :
Polynomial.coeff recurrence4Scalar0Left 24 = -(4593276624478587063442805627586039543 * 10 ^ 70 + 5646380173268724972492095228311240760832707924102554758634350466314540)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_25 :
Polynomial.coeff recurrence4Scalar0Left 25 = 314575394241842978066401606684469886961 * 10 ^ 70 + 1862660831899487752141058172230858260149791746714504580968234561886289
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_26 :
Polynomial.coeff recurrence4Scalar0Left 26 = 90188739822873726597645640712345975407336 * 10 ^ 70 + 1848408656321956770453570574339366768476405372777930598330545271736192
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_27 :
Polynomial.coeff recurrence4Scalar0Left 27 = -(47472945155781104805881557576272279970829270 * 10 ^ 70 + 2463096933659531822014426013344799255186839795914061129044617960421811)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_28 :
Polynomial.coeff recurrence4Scalar0Left 28 = 14860783678875038475650658693032404309568113452 * 10 ^ 70 + 5062683973086312434130255268409539615405407396157439143558632436092881
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_29 :
Polynomial.coeff recurrence4Scalar0Left 29 = -(4009486755537940051369205241685237169159833060881 * 10 ^ 70 + 448703897744713800821481200751062039777913283766194757810194023803389)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_30 :
Polynomial.coeff recurrence4Scalar0Left 30 = 991325432159248126817767444863576661726970409518664 * 10 ^ 70 + 4763689709160270247270502862119605829291747742375935454158963160288750
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_31 :
Polynomial.coeff recurrence4Scalar0Left 31 = -(222766125487281248884502158755589038328448550491205800 * 10 ^ 70 + 1732260284052116144575532853231655950920389723961399212879042225177039)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_32 :
Polynomial.coeff recurrence4Scalar0Left 32 = 44654929890076778110346828028692245495767061942482502850 * 10 ^ 70 + 9417726356810555127461233760149721944452682589147747084437460840662033
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_33 :
Polynomial.coeff recurrence4Scalar0Left 33 = -(7877649534575521649089888418514468349733659212204717866770 * 10 ^ 70 + 257681197005537610461666333360155361191864936945338246990357637870317)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_34 :
Polynomial.coeff recurrence4Scalar0Left 34 = 1210150920670225404857902116339205835451828513386344410711212 * 10 ^ 70 + 5020537940021549941084547637431724497652189958663978125833307096499263
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_35 :
Polynomial.coeff recurrence4Scalar0Left 35 = -(159485364398050669542907902859913061578058157789376412863813304 * 10 ^ 70 + 1738351069935894636310465606624129546626499136616744153639226421855041)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_36 :
Polynomial.coeff recurrence4Scalar0Left 36 = 17458997617944449493306055401334744682602380812007448103014489114 * 10 ^ 70 + 5511737695482662806494079848332735542441768643389567749115293230932648
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_37 :
Polynomial.coeff recurrence4Scalar0Left 37 = -(1450115538334776121332783482490118770744671801039095164210020281860 * 10 ^ 70 + 5266512070043421813760936156384710075046265452476702169354751172738612)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_38 :
Polynomial.coeff recurrence4Scalar0Left 38 = 58134567135023988216705502136830159585781645463308808683750438152361 * 10 ^ 70 + 2283782458052865862753310909554860781095660971061656856013732510959743
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_39 :
Polynomial.coeff recurrence4Scalar0Left 39 = 7983218316488806869114638024823357249500098812071243105188393523812287 * 10 ^ 70 + 1188855890801962168088383809422999183328926029879898674033569873877527
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Left_coeff_40 :
Polynomial.coeff recurrence4Scalar0Left 40 = -((240 * 10 ^ 70 + 4111273167440109873820575764523366089483163955615204110000101011596498) * 10 ^ 70 + 9011788551168566615622936198576158482118123357198785910778896620661411)