Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB4High

Recurrence 2 lookup certificate: B4 source coefficients, high 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_70 :
Polynomial.coeff remainder3Coefficient4 70 = 72293 * 10 ^ 70 + 6546298955043341803801756707295402481722750762138409272635463114366872
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_71 :
Polynomial.coeff remainder3Coefficient4 71 = -(188249 * 10 ^ 70 + 8264228494952716897055549192866735040549568852464851571751607254133648)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_72 :
Polynomial.coeff remainder3Coefficient4 72 = 299353 * 10 ^ 70 + 3819118038278918281363506249228537160055307838046960865932584877026862
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_73 :
Polynomial.coeff remainder3Coefficient4 73 = -(823 * 10 ^ 70 + 2324130292502960379709079989235617404803803740994462067480843269586572)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_74 :
Polynomial.coeff remainder3Coefficient4 74 = -(2002226 * 10 ^ 70 + 5532399621233984515829052094075829741564337127897599399293694349930041)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_75 :
Polynomial.coeff remainder3Coefficient4 75 = 8841339 * 10 ^ 70 + 6433040341167382275939927070307274891756469640623047195629519480931904
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_76 :
Polynomial.coeff remainder3Coefficient4 76 = -(26752321 * 10 ^ 70 + 3229486000588140745357639417363400005006489730779474069838766336181069)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_77 :
Polynomial.coeff remainder3Coefficient4 77 = 66256622 * 10 ^ 70 + 540898441314124627966305086727507212463405811337169716214565403849511
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_78 :
Polynomial.coeff remainder3Coefficient4 78 = -(142455896 * 10 ^ 70 + 722572213083076822628651932983979906175362937045217674479908435327793)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_79 :
Polynomial.coeff remainder3Coefficient4 79 = 273438549 * 10 ^ 70 + 6769727566161581142791822932842932319131230956667858814263202751532890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_80 :
Polynomial.coeff remainder3Coefficient4 80 = -(476106768 * 10 ^ 70 + 9242154024196020089052684996121630353982565142785233562563126702221069)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_81 :
Polynomial.coeff remainder3Coefficient4 81 = 759711321 * 10 ^ 70 + 2604784453966461208054289680894457147649477622894193858695088995530860
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_82 :
Polynomial.coeff remainder3Coefficient4 82 = -(1118790302 * 10 ^ 70 + 7318136317892063105151494098427299971270368139630649483172552208778120)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_83 :
Polynomial.coeff remainder3Coefficient4 83 = 1528362978 * 10 ^ 70 + 2885341592599066200522128164017201648705113795779833317934912873796661
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_84 :
Polynomial.coeff remainder3Coefficient4 84 = -(1944294602 * 10 ^ 70 + 4757985943605790594512323681137252438779763104278384719484780488590953)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_85 :
Polynomial.coeff remainder3Coefficient4 85 = 2310276253 * 10 ^ 70 + 6526530175042687455315692981900230669699816352895023190744212553846896
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_86 :
Polynomial.coeff remainder3Coefficient4 86 = -(2570244438 * 10 ^ 70 + 3954427859365006550288294893519496392718208009886080739156081891640020)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_87 :
Polynomial.coeff remainder3Coefficient4 87 = 2682488861 * 10 ^ 70 + 366718263831293466549513020610567578482050277295338704570109519554635
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_88 :
Polynomial.coeff remainder3Coefficient4 88 = -(2630546229 * 10 ^ 70 + 3125612643666967621719007779474712200568671476586209363934903873224876)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_89 :
Polynomial.coeff remainder3Coefficient4 89 = 2426988208 * 10 ^ 70 + 23183135037612333027384563202292542989885251222176691684716872086862
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_90 :
Polynomial.coeff remainder3Coefficient4 90 = -(2108969149 * 10 ^ 70 + 6150868430004524959658346988303085720770418499213225587943674114347325)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_91 :
Polynomial.coeff remainder3Coefficient4 91 = 1727553064 * 10 ^ 70 + 114236332374562784641045449023565067420300617594329962760964940673928
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_92 :
Polynomial.coeff remainder3Coefficient4 92 = -(1334893421 * 10 ^ 70 + 9073107537917657924673541044166478524743153344467397622935895465968103)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_93 :
Polynomial.coeff remainder3Coefficient4 93 = 973489500 * 10 ^ 70 + 8149408062168356571431319160608670726118985984697123650828547752018559
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_94 :
Polynomial.coeff remainder3Coefficient4 94 = -(670223475 * 10 ^ 70 + 4006282755541930446584470691098991528066949365306902317341463337966194)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_95 :
Polynomial.coeff remainder3Coefficient4 95 = 435672836 * 10 ^ 70 + 579080087452820107525544644139704221831271942433855889810419879884016
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_96 :
Polynomial.coeff remainder3Coefficient4 96 = -(267368983 * 10 ^ 70 + 972626075423450472368080268086739992817154259640557109519060905273751)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_97 :
Polynomial.coeff remainder3Coefficient4 97 = 154856528 * 10 ^ 70 + 1952401353923621140015727192261910648679321021515264273411052448818224
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_98 :
Polynomial.coeff remainder3Coefficient4 98 = -(84599459 * 10 ^ 70 + 5728345182596141854462786209664878600017983372710734323642311215374515)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_99 :
Polynomial.coeff remainder3Coefficient4 99 = 43557504 * 10 ^ 70 + 8336836472621610767820516862020740232837272957862852338290272287766724
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_100 :
Polynomial.coeff remainder3Coefficient4 100 = -(21112196 * 10 ^ 70 + 7249118397836152595743629594069474390351770707469294858648029819087685)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_101 :
Polynomial.coeff remainder3Coefficient4 101 = 9619923 * 10 ^ 70 + 3965322760559251076344293145718571794832419172303977393639571369492580
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_102 :
Polynomial.coeff remainder3Coefficient4 102 = -(4113785 * 10 ^ 70 + 7746372218996284722706293423986162949322000514207473524877579591333294)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_103 :
Polynomial.coeff remainder3Coefficient4 103 = 1647692 * 10 ^ 70 + 5669392800475144901255982804517082150241506891099890558296924694399012
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_104 :
Polynomial.coeff remainder3Coefficient4 104 = -(616699 * 10 ^ 70 + 452048539346543409145632237018487591852511559680114191645744126560511)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_105 :
Polynomial.coeff remainder3Coefficient4 105 = 215125 * 10 ^ 70 + 8734518826383342587870083294359383538963615383112838220694365279350594
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_106 :
Polynomial.coeff remainder3Coefficient4 106 = -(69734 * 10 ^ 70 + 7636728465043085077910103437617362691990986754589176341788777091409973)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_107 :
Polynomial.coeff remainder3Coefficient4 107 = 20936 * 10 ^ 70 + 4971475766633264194787104501300545407508134365709600123953770398958610
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_108 :
Polynomial.coeff remainder3Coefficient4 108 = -(5800 * 10 ^ 70 + 2749491038843155142605709413798589843284619608769324948135258266948481)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_109 :
Polynomial.coeff remainder3Coefficient4 109 = 1476 * 10 ^ 70 + 6768496062207618124554460556092810898302231359398966351689027232147725
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_110 :
Polynomial.coeff remainder3Coefficient4 110 = -(343 * 10 ^ 70 + 8741078067813006999964111558802515650913563001272199381738696663260175)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_111 :
Polynomial.coeff remainder3Coefficient4 111 = 72 * 10 ^ 70 + 8651688557667569717560257497291319857445016512279007790599929826497054
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_112 :
Polynomial.coeff remainder3Coefficient4 112 = -(13 * 10 ^ 70 + 9659714224592769635984264760056782903951715702256776404717511245505575)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_113 :
Polynomial.coeff remainder3Coefficient4 113 = 2 * 10 ^ 70 + 4049548201996091490503564997300121330517421945187119738711493174145342
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_114 :
Polynomial.coeff remainder3Coefficient4 114 = -3691694611221366274457078411542491964204073636130756575140474765809139
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_115 :
Polynomial.coeff remainder3Coefficient4 115 = 500562717063577489490331790070398938980262126112598798225496500501679
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_116 :
Polynomial.coeff remainder3Coefficient4 116 = -59308767984437397009771699399855183112786431021313900982449145260424
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_117 :
Polynomial.coeff remainder3Coefficient4 117 = 6061805810475100842236192944724333454945927691876451661768457509208
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_118 :
Polynomial.coeff remainder3Coefficient4 118 = -526146696073771114129468010201317951983904526345399239456287295778
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_119 :
Polynomial.coeff remainder3Coefficient4 119 = 38040539816116776731133440544087903974097916940432998240197912828
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_120 :
Polynomial.coeff remainder3Coefficient4 120 = -2236071424626926695964541350283361969758705262391755786029701063
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_121 :
Polynomial.coeff remainder3Coefficient4 121 = 103583270207729848252855016478559194645919148297368310956552733
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_122 :
Polynomial.coeff remainder3Coefficient4 122 = -3628696384037984960252045373735553196736232430519501983629386
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_123 :
Polynomial.coeff remainder3Coefficient4 123 = 90789408065674999168409458609903686043489473381768803237326
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_124 :
Polynomial.coeff remainder3Coefficient4 124 = -1486886117090757955611969937896437602163161758729217465430
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_125 :
Polynomial.coeff remainder3Coefficient4 125 = 13464155310162441795021689648575150520982710456067865301
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_126 :
Polynomial.coeff remainder3Coefficient4 126 = -32477957755995909479046641812234839673995332546198744
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_127 :
Polynomial.coeff remainder3Coefficient4 127 = -412510088768745846689445454736320617589341970511378
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_128 :
Polynomial.coeff remainder3Coefficient4 128 = 2816636253566328745715348205629681472013754323165
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_129 :
Polynomial.coeff remainder3Coefficient4 129 = -1618028819840626949148439626073625377555435387
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_130 :
Polynomial.coeff remainder3Coefficient4 130 = -26735832861833083505215688216277786586607238
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_131 :
Polynomial.coeff remainder3Coefficient4 131 = 75348378164637813971372304330837750740845
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_132 :
Polynomial.coeff remainder3Coefficient4 132 = -76049583511674624112600037709819546500
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_133 :
Polynomial.coeff remainder3Coefficient4 133 = 29466558674585668368175858912839223
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_134 :
Polynomial.coeff remainder3Coefficient4 134 = -3762970816376932961872264762260
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_135 :
Polynomial.coeff remainder3Coefficient4 135 = 121657735088933848098082139
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_136 :
Polynomial.coeff remainder3Coefficient4 136 = -655632661571987784261
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_137 :
Polynomial.coeff remainder3Coefficient4 137 = 280915358490100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B4_coeff_138 :
Polynomial.coeff remainder3Coefficient4 138 = -794588