Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB5Low

Recurrence 2 lookup certificate: B5 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.recurrence2B5_coeff_0 :
Polynomial.coeff remainder3Coefficient5 0 = 64
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_1 :
Polynomial.coeff remainder3Coefficient5 1 = -12156
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_2 :
Polynomial.coeff remainder3Coefficient5 2 = 1354562202
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_3 :
Polynomial.coeff remainder3Coefficient5 3 = -518380813692
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_4 :
Polynomial.coeff remainder3Coefficient5 4 = 585555622533882
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_5 :
Polynomial.coeff remainder3Coefficient5 5 = -157410261428692160
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_6 :
Polynomial.coeff remainder3Coefficient5 6 = 34556515582732965276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_7 :
Polynomial.coeff remainder3Coefficient5 7 = -4301410760970204622105
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_8 :
Polynomial.coeff remainder3Coefficient5 8 = 384185146583496783398731
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_9 :
Polynomial.coeff remainder3Coefficient5 9 = -23102340457255115206225180
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_10 :
Polynomial.coeff remainder3Coefficient5 10 = 1023234497103504062614474552
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_11 :
Polynomial.coeff remainder3Coefficient5 11 = -33268964950842174920443327383
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_12 :
Polynomial.coeff remainder3Coefficient5 12 = 758633249959525901109917614448
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_13 :
Polynomial.coeff remainder3Coefficient5 13 = 1507484628252244886952455312383
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_14 :
Polynomial.coeff remainder3Coefficient5 14 = -1597478344599563677298840073878171
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_15 :
Polynomial.coeff remainder3Coefficient5 15 = 116373838883438904938614640656704955
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_16 :
Polynomial.coeff remainder3Coefficient5 16 = -5366032119857615523081935066061634679
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_17 :
Polynomial.coeff remainder3Coefficient5 17 = 181168266321197660865678430073531837421
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_18 :
Polynomial.coeff remainder3Coefficient5 18 = -4688268113965608702130455099134678375699
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_19 :
Polynomial.coeff remainder3Coefficient5 19 = 94242606004781941951845106722309539305573
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_20 :
Polynomial.coeff remainder3Coefficient5 20 = -1443692377612875362915310937684463618654664
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_21 :
Polynomial.coeff remainder3Coefficient5 21 = 15220765080512840366464686731227324522190291
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_22 :
Polynomial.coeff remainder3Coefficient5 22 = -51709534414231195056832264154795877180578015
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_23 :
Polynomial.coeff remainder3Coefficient5 23 = -2088691358881307945602799163382309623604857558
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_24 :
Polynomial.coeff remainder3Coefficient5 24 = 62112663824049410516588572312860692397002375981
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_25 :
Polynomial.coeff remainder3Coefficient5 25 = -1096152708335522347033464127465701902955878650206
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_26 :
Polynomial.coeff remainder3Coefficient5 26 = 14948017681121838016616867722378586391672891499004
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_27 :
Polynomial.coeff remainder3Coefficient5 27 = -169500399305199683132202717770969364728771132566079
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_28 :
Polynomial.coeff remainder3Coefficient5 28 = 1651019051308693417631201608933808494457423689764077
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_29 :
Polynomial.coeff remainder3Coefficient5 29 = -14063627383815414127233100855777399941339125040500099
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_30 :
Polynomial.coeff remainder3Coefficient5 30 = 105917189634355617289564490597701936033350055464950937
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_31 :
Polynomial.coeff remainder3Coefficient5 31 = -710165696978516089964604718979335271731610544719841884
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_32 :
Polynomial.coeff remainder3Coefficient5 32 = 4256548100224837219944082284559531223048156335571915446
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_33 :
Polynomial.coeff remainder3Coefficient5 33 = -22848238885305523165302020957055047654566058350901061154
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_34 :
Polynomial.coeff remainder3Coefficient5 34 = 109789128754097385507407932976912040088068164627896663603
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_35 :
Polynomial.coeff remainder3Coefficient5 35 = -470661950176926338602388446111629162245194919375373530551
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_36 :
Polynomial.coeff remainder3Coefficient5 36 = 1785017533754185844634067673117507157955536654718105276975
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_37 :
Polynomial.coeff remainder3Coefficient5 37 = -5877578946285211009667169735200547441309488908296664940137
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_38 :
Polynomial.coeff remainder3Coefficient5 38 = 16073844166706592948672022590492243118351718016347366895539
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_39 :
Polynomial.coeff remainder3Coefficient5 39 = -31972063857397936867818279330587369649806597070346540161288
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_40 :
Polynomial.coeff remainder3Coefficient5 40 = 16526830343414984442770481395649957371359772004219738968345
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_41 :
Polynomial.coeff remainder3Coefficient5 41 = 232874833269767410146557178501078408661719140279534891310910
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_42 :
Polynomial.coeff remainder3Coefficient5 42 = -1483268019190884257892954689205167345399660826585251827140150
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_43 :
Polynomial.coeff remainder3Coefficient5 43 = 6153412297890782315442632121625329952107476035612251127804010
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_44 :
Polynomial.coeff remainder3Coefficient5 44 = -21050635779083919515488972262208135117165390212869305927476258
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_45 :
Polynomial.coeff remainder3Coefficient5 45 = 62627862336168020614276340147971039322194268518301393583264248
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_46 :
Polynomial.coeff remainder3Coefficient5 46 = -156650913352348315895120015905858960763193998994036032611684592
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_47 :
Polynomial.coeff remainder3Coefficient5 47 = 288605086662484691375303631867463597517122484614948498510881529
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_48 :
Polynomial.coeff remainder3Coefficient5 48 = -274939148849570046895308170617336734246000723960126787775642912
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_49 :
Polynomial.coeff remainder3Coefficient5 49 = 152350745627287390737076952925818039970546316231009997001622265
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_50 :
Polynomial.coeff remainder3Coefficient5 50 = -3675919368687448028956551421543945784774951429554339175838887131
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_51 :
Polynomial.coeff remainder3Coefficient5 51 = 24718253578327531557654063039275426081028169217687267035479497655
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_52 :
Polynomial.coeff remainder3Coefficient5 52 = -55400300387709814704672048624214403986754900782173671569889578366
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_53 :
Polynomial.coeff remainder3Coefficient5 53 = -157374571515781813053417558657762161533945946317239716557761927688
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_54 :
Polynomial.coeff remainder3Coefficient5 54 = 1534714190196044122729144518082790927485218819424997583811024485594
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_55 :
Polynomial.coeff remainder3Coefficient5 55 = -4282329269304493210767701528326420236321334042909988444148947142377
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_56 :
Polynomial.coeff remainder3Coefficient5 56 = -3041267233044429338394683166576711604150740321675024639781277390349
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_57 :
Polynomial.coeff remainder3Coefficient5 57 = 69524738659047282022855197487281119144351180244689394823464662944194
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_58 :
Polynomial.coeff remainder3Coefficient5 58 = -255969526666785140037704816165129538592843787358204745662036357188846
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_59 :
Polynomial.coeff remainder3Coefficient5 59 = 241457309966006350374379727158419282784868344869176178406301862034607
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_60 :
Polynomial.coeff remainder3Coefficient5 60 = 1955858626746270931855404397872885430919663983795806797029695044989887
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_61 :
Polynomial.coeff remainder3Coefficient5 61 = -(1 * 10 ^ 70 + 1051349933467088165738058933963914517770030080980683601082305893458160)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_62 :
Polynomial.coeff remainder3Coefficient5 62 = 2 * 10 ^ 70 + 6400172437023117610899553651518033237685125014432822917090407935153063
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_63 :
Polynomial.coeff remainder3Coefficient5 63 = -91318310931367026818465719861175689272173472685573552275420049939245
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_64 :
Polynomial.coeff remainder3Coefficient5 64 = -(25 * 10 ^ 70 + 8532857061551560619365614597404627507404602945638687838891821075609611)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_65 :
Polynomial.coeff remainder3Coefficient5 65 = 111 * 10 ^ 70 + 4163830836147869011439870007577002678406117261980631161822979234983019
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_66 :
Polynomial.coeff remainder3Coefficient5 66 = -(247 * 10 ^ 70 + 9240447283096022041103532283391225269761211109368923961149915724191930)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B5_coeff_67 :
Polynomial.coeff remainder3Coefficient5 67 = 110 * 10 ^ 70 + 2611223183233577487645478890032845953513110067800062998680582546465865