Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB4Low

Recurrence 2 lookup certificate: B4 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.recurrence2B4_coeff_0 :
Polynomial.coeff remainder3Coefficient4 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_1 :
Polynomial.coeff remainder3Coefficient4 1 = -488
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_2 :
Polynomial.coeff remainder3Coefficient4 2 = 79908936
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_3 :
Polynomial.coeff remainder3Coefficient4 3 = -54171772584
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_4 :
Polynomial.coeff remainder3Coefficient4 4 = 74645004683336
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_5 :
Polynomial.coeff remainder3Coefficient4 5 = -29051618894656499
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_6 :
Polynomial.coeff remainder3Coefficient4 6 = 7886790788452359315
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_7 :
Polynomial.coeff remainder3Coefficient4 7 = -1278370368188845513764
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_8 :
Polynomial.coeff remainder3Coefficient4 8 = 140987840827161338457851
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_9 :
Polynomial.coeff remainder3Coefficient4 9 = -10701779933849849433844089
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_10 :
Polynomial.coeff remainder3Coefficient4 10 = 588152189587661323715172081
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_11 :
Polynomial.coeff remainder3Coefficient4 11 = -24167814127891687580020207335
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_12 :
Polynomial.coeff remainder3Coefficient4 12 = 729195980181088218206280942700
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_13 :
Polynomial.coeff remainder3Coefficient4 13 = -8895471790438980058846996164913
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_14 :
Polynomial.coeff remainder3Coefficient4 14 = -882612127378855411361653196714648
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_15 :
Polynomial.coeff remainder3Coefficient4 15 = 89365878071942030982913958852886304
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_16 :
Polynomial.coeff remainder3Coefficient4 16 = -4923582587274649083139695798829936769
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_17 :
Polynomial.coeff remainder3Coefficient4 17 = 193360427385813188975621594468990858686
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_18 :
Polynomial.coeff remainder3Coefficient4 18 = -5788532679887554975261205198967747686851
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_19 :
Polynomial.coeff remainder3Coefficient4 19 = 135288248224309717839398853453681221533696
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_20 :
Polynomial.coeff remainder3Coefficient4 20 = -2462609013470166402268531714867748618199639
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_21 :
Polynomial.coeff remainder3Coefficient4 21 = 33339758442488426345554443264033565017930115
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_22 :
Polynomial.coeff remainder3Coefficient4 22 = -270679302557652162589462507020207511690718005
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_23 :
Polynomial.coeff remainder3Coefficient4 23 = -1008818495035685879478047562937998290862155503
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_24 :
Polynomial.coeff remainder3Coefficient4 24 = 87859518738094204518914861028615064599069473206
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_25 :
Polynomial.coeff remainder3Coefficient4 25 = -1996446506939477995085583788522015464054736054877
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_26 :
Polynomial.coeff remainder3Coefficient4 26 = 32007005156281181505856727509883767105293103004514
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_27 :
Polynomial.coeff remainder3Coefficient4 27 = -414475844456614144844151244654497319796243288778674
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_28 :
Polynomial.coeff remainder3Coefficient4 28 = 4553400933006248078802631154823702817095792105900271
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_29 :
Polynomial.coeff remainder3Coefficient4 29 = -43490965361797663125814311585276534845596882357840770
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_30 :
Polynomial.coeff remainder3Coefficient4 30 = 366411820327147359441537506283766953887904168172066702
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_31 :
Polynomial.coeff remainder3Coefficient4 31 = -2748502211711448991639651408908403456731970402167966495
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_32 :
Polynomial.coeff remainder3Coefficient4 32 = 18470328906533137619902866800115673246183364037582400911
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_33 :
Polynomial.coeff remainder3Coefficient4 33 = -111648682526514395867932171694428172751902103118003413560
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_34 :
Polynomial.coeff remainder3Coefficient4 34 = 608432329238316096883754444681345561559019896743515021197
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_35 :
Polynomial.coeff remainder3Coefficient4 35 = -2990695177461363061406833255061234766763411781951336165514
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_36 :
Polynomial.coeff remainder3Coefficient4 36 = 13237718815493998019899288784617610290798803012441576727343
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_37 :
Polynomial.coeff remainder3Coefficient4 37 = -52502605798787872119996775014233460522634368465938442985043
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_38 :
Polynomial.coeff remainder3Coefficient4 38 = 184579337456064638954568715230795236941493505519635632580955
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_39 :
Polynomial.coeff remainder3Coefficient4 39 = -562236680128760107962573419031430712207619710315337358381305
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_40 :
Polynomial.coeff remainder3Coefficient4 40 = 1406307149455739623594356861532069650456895070659381148711193
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_41 :
Polynomial.coeff remainder3Coefficient4 41 = -2423850189762669748208799419426172192321523993140498066104006
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_42 :
Polynomial.coeff remainder3Coefficient4 42 = -197336827839669322632473451657661860781238967613539597953615
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_43 :
Polynomial.coeff remainder3Coefficient4 43 = 24854031952164914996894325056269314301931991893396923723541266
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_44 :
Polynomial.coeff remainder3Coefficient4 44 = -138215545453863210538475321355045517286365246515311416313462181
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_45 :
Polynomial.coeff remainder3Coefficient4 45 = 542576334946524184941790668853533285102927230254261096629654661
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_46 :
Polynomial.coeff remainder3Coefficient4 46 = -1755657688136356897476181133016516604599131969331912417823621915
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_47 :
Polynomial.coeff remainder3Coefficient4 47 = 4824953892101361868840861253802219905285789358070456586664162781
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_48 :
Polynomial.coeff remainder3Coefficient4 48 = -11188907154916730751431668524239029812334343868615229025696267272
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_49 :
Polynomial.coeff remainder3Coefficient4 49 = 22159876195200541825288614976241194304914096854983463400518814819
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_50 :
Polynomial.coeff remainder3Coefficient4 50 = -43878357774793283803705695084308372379342153863154742382676829337
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_51 :
Polynomial.coeff remainder3Coefficient4 51 = 116168706880217995187833923198595633714237637222029887934310148860
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_52 :
Polynomial.coeff remainder3Coefficient4 52 = -331531685124414616494006930352859635083193832697486716593344284348
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_53 :
Polynomial.coeff remainder3Coefficient4 53 = 416781706939311167391295573343303108140942582076923175022422653348
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_54 :
Polynomial.coeff remainder3Coefficient4 54 = 2288057942395516301874537037127348688860236592066239956523068698194
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_55 :
Polynomial.coeff remainder3Coefficient4 55 = -15027005393041491111291775726982408973660731111581889612795188198276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_56 :
Polynomial.coeff remainder3Coefficient4 56 = 31205787281616005358739491370661912562932163198191396863724752762504
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_57 :
Polynomial.coeff remainder3Coefficient4 57 = 70824160951855985857684626573077506889865415795629591025559933421298
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_58 :
Polynomial.coeff remainder3Coefficient4 58 = -704329761420437485860504450663813125601364110836143296241149336499616
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_59 :
Polynomial.coeff remainder3Coefficient4 59 = 2096673518452005734254197699408252886561028548057257693744437477509923
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_60 :
Polynomial.coeff remainder3Coefficient4 60 = -429095125300578788538477178154569570773685060326131013651589371659683
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_61 :
Polynomial.coeff remainder3Coefficient4 61 = -(2 * 10 ^ 70 + 2492281016135882505333965254250250313578373468918714135682932527214861)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_62 :
Polynomial.coeff remainder3Coefficient4 62 = 10 * 10 ^ 70 + 1558558039385865222836294369420977249002541350024726686687301932041169
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_63 :
Polynomial.coeff remainder3Coefficient4 63 = -(19 * 10 ^ 70 + 8652577094721135931073178264219316140899172164130278500653729568501592)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_64 :
Polynomial.coeff remainder3Coefficient4 64 = -(17 * 10 ^ 70 + 6565239946859853473116379656727546168794978080509620418351549224155658)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_65 :
Polynomial.coeff remainder3Coefficient4 65 = 270 * 10 ^ 70 + 2953007588566631629174960270157122332606142430035329079709240392592458
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_66 :
Polynomial.coeff remainder3Coefficient4 66 = -(1006 * 10 ^ 70 + 3842118408960246637724608263283382533914182735720419176302758058387438)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_67 :
Polynomial.coeff remainder3Coefficient4 67 = 1945 * 10 ^ 70 + 6360616319541174764935443622590468639352927797789194888322544251300231
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_68 :
Polynomial.coeff remainder3Coefficient4 68 = 192 * 10 ^ 70 + 2214155732299846269579554624683053779207647506245495350597584069315180
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_69 :
Polynomial.coeff remainder3Coefficient4 69 = -(16893 * 10 ^ 70 + 9163095657195668981069001406276089211626802206649683371629930986218430)