Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1MainPart0.Coefficients154To194

Recurrence 2 lookup certificate: Scalar1Main coefficient convolution #

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.recurrence2Scalar1Main_coeff_154 :
Polynomial.coeff recurrence2Scalar1Main 154 = (6461298735042580221388147636178609526243994 * 10 ^ 70 + 1823914070232730133196736269649483127784233544145496502572666663208494) * 10 ^ 70 + 4005582501138958191715652658085615540000345536354631767796462221420504
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_155 :
Polynomial.coeff recurrence2Scalar1Main 155 = -((32057109161512211267880860158470997154857680 * 10 ^ 70 + 9854959910511824707394309074410592716380514069134916322030757464578055) * 10 ^ 70 + 4320202776143798948667031246006909976842283031824832274677134589946336)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_156 :
Polynomial.coeff recurrence2Scalar1Main 156 = (40410751332417383306088611255581383782263330 * 10 ^ 70 + 9811918877147443879018694133803800987901532203018902023307674096941037) * 10 ^ 70 + 9006674347083825761735955079570252894184162716533650205165020910005863
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_157 :
Polynomial.coeff recurrence2Scalar1Main 157 = (236299777750241645303862309752795605761560462 * 10 ^ 70 + 6474845719827529330912019693588633300556991905202694927909916445760094) * 10 ^ 70 + 2673404219272698587395041620113326162585218846698356135803469106726828
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_158 :
Polynomial.coeff recurrence2Scalar1Main 158 = -((1347640255539764947946691698779225850866801894 * 10 ^ 70 + 4572651915294032403306379477418153307794972859105881034761711658684706) * 10 ^ 70 + 5925607380880674758900332812185069785533715996544683993573380065115253)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_159 :
Polynomial.coeff recurrence2Scalar1Main 159 = (2179653922662608520778315096500915350057889456 * 10 ^ 70 + 4950284567430017927668880953905763953185923722565308100496922541690027) * 10 ^ 70 + 918712493448324643256296005456452633228509247656511057010987765994080
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_160 :
Polynomial.coeff recurrence2Scalar1Main 160 = (7543597192803764399063484686209209774716801258 * 10 ^ 70 + 4844080024556631462777294608175484384978512625322685271825537929147651) * 10 ^ 70 + 1962031499174315669844464295809255554617345394414394519660145786628824
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_161 :
Polynomial.coeff recurrence2Scalar1Main 161 = -((52259668065325313881124228230598359699689398061 * 10 ^ 70 + 6997675819770182780215232728997539560237382920819924113713423391122739) * 10 ^ 70 + 3930650813782259039107571377980612032724837052135412670427931148046649)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_162 :
Polynomial.coeff recurrence2Scalar1Main 162 = (105604672266143078746695134798957358107112744577 * 10 ^ 70 + 1949790807626654688318098667867436570217860453510360245431976969828635) * 10 ^ 70 + 1419405861001809949383122662094942266509750711217652078840283939375409
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_163 :
Polynomial.coeff recurrence2Scalar1Main 163 = (197450152999801774511692288859108422715335482555 * 10 ^ 70 + 6830784712336936650395533143406093240335075141596508784388268661412949) * 10 ^ 70 + 4641723045972674012501537834361721702740965388138447194024752443452015
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_164 :
Polynomial.coeff recurrence2Scalar1Main 164 = -((1899299245591878911801021492133396472091928706467 * 10 ^ 70 + 9580254641458886943377044869287602426775451494122781933309758875708175) * 10 ^ 70 + 4467911678717042931532193809739921353111688141946052974509824345454722)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_165 :
Polynomial.coeff recurrence2Scalar1Main 165 = (4888835184961910833687173449837226217087349309504 * 10 ^ 70 + 9626025075332291337806994412904988624339373348967783986639594034891898) * 10 ^ 70 + 9784185589553288317883981882678361344420473732992531397797715007141669
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_166 :
Polynomial.coeff recurrence2Scalar1Main 166 = (2315594149101257414919220163514494530334985564816 * 10 ^ 70 + 7688661541367878898198962112086454084838847336306077118221110715373643) * 10 ^ 70 + 8496950943546086478283992381322173295675311511867390357859457308973742
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_167 :
Polynomial.coeff recurrence2Scalar1Main 167 = -((61093790645123425665359553910475023144954535720485 * 10 ^ 70 + 1835670683611179078480037131641732108025795197881129347094953606710310) * 10 ^ 70 + 803814546809944739690079389707120327509792833828727909483425151072312)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_168 :
Polynomial.coeff recurrence2Scalar1Main 168 = (207299104687642405243588143602790461373188802298521 * 10 ^ 70 + 4488145114243280964897465061870433221562638811399590621046994797032236) * 10 ^ 70 + 1531647540837404064819041870617683927797051691804550077276056757549481
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_169 :
Polynomial.coeff recurrence2Scalar1Main 169 = -((156440486402784575164762570509014717003709468035747 * 10 ^ 70 + 315905530857593403225558037140754763510837568430363865836951373338292) * 10 ^ 70 + 415643237726015284632570374176100011316250395404384911283332961965451)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_170 :
Polynomial.coeff recurrence2Scalar1Main 170 = -((1512775525845693157865526899211757271257533001485942 * 10 ^ 70 + 6132063286804707369432402830657840113124969464579921093293241590390386) * 10 ^ 70 + 3646248492656938109821925093958399831810236047861713953511462699416242)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_171 :
Polynomial.coeff recurrence2Scalar1Main 171 = (7361653280122369814786670613817354068989131270570630 * 10 ^ 70 + 6276689965701426388568801721895269824240730446354818103343909189150454) * 10 ^ 70 + 1009622607415600713772378176778292819614747174040455659040871069242059
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_172 :
Polynomial.coeff recurrence2Scalar1Main 172 = -((13432681598432238197546702599615906506717618475362366 * 10 ^ 70 + 4380332053383636921674968968516702691160598208357135153466067905951733) * 10 ^ 70 + 4568437569214117834651454073251106594084161829326498617551780996250442)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_173 :
Polynomial.coeff recurrence2Scalar1Main 173 = -((19132004189532396160526515732308522121635640718838726 * 10 ^ 70 + 2349700309839966753688182086633057813009535884098558814385452241849528) * 10 ^ 70 + 4154303892298943775341524818892618896422542276407901105324408847235182)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_174 :
Polynomial.coeff recurrence2Scalar1Main 174 = (199933415931712364657006698905184614190760136323406411 * 10 ^ 70 + 4670585267948563952761164754945673955940672153352372359475538082787599) * 10 ^ 70 + 4182122088919007742975389151561478035852808058543403929552407358550145
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_175 :
Polynomial.coeff recurrence2Scalar1Main 175 = -((590264693082111170512776917691840075891950891784572877 * 10 ^ 70 + 6588363023782066506215936882296572101950425697994991609493512078046722) * 10 ^ 70 + 1736273383673102616106274507495115441323245966018601777795086357372705)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_176 :
Polynomial.coeff recurrence2Scalar1Main 176 = (450268885834677150699332929463796122598413251627417051 * 10 ^ 70 + 5857365059473078029299091307777618429552300376939333707936924062967530) * 10 ^ 70 + 5854109521403605026340670468929899080544955889620709197743884489719185
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_177 :
Polynomial.coeff recurrence2Scalar1Main 177 = (3530969930929979358488832973216346575749058081359314193 * 10 ^ 70 + 2595847068076732929031756637154139975559271453935678809785129879028905) * 10 ^ 70 + 8354338658661173165865726809346816127475077540141874861671126716516762
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_178 :
Polynomial.coeff recurrence2Scalar1Main 178 = -((17470230401364356729209450458207917107825229258435049461 * 10 ^ 70 + 5537064211807583066892101638362929465776870125427784341860954287585470) * 10 ^ 70 + 2782373117251168406840667544872130117709391706715388293444786230781830)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_179 :
Polynomial.coeff recurrence2Scalar1Main 179 = (36563816802827254906999330982289885296102554076321004946 * 10 ^ 70 + 5303660717383220971686107336623436623843777583068230798904019101454936) * 10 ^ 70 + 8017762500278147814507994902630317776022372282599389379609908446511128
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_180 :
Polynomial.coeff recurrence2Scalar1Main 180 = (7707571802957994719435051300017745937072301931314703037 * 10 ^ 70 + 5898744499671878067701612196509660815824204363794090796100983677469370) * 10 ^ 70 + 4565173202330357441834703225473757635077160068567813402311621186474245
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_181 :
Polynomial.coeff recurrence2Scalar1Main 181 = -((334220964268205646597320604136302406535350809016865175052 * 10 ^ 70 + 7345050835429703450374587870091514054917393083250324433813673418410141) * 10 ^ 70 + 2543407657281567517669950487633001181320839133785873172553000802816739)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_182 :
Polynomial.coeff recurrence2Scalar1Main 182 = (1221201560455158147001143325682852828901844090458111097100 * 10 ^ 70 + 1589839235019346043899461466742384752006611723833250383627134399136651) * 10 ^ 70 + 9302373865877268113487880273959879630257188098689101974882464034826097
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_183 :
Polynomial.coeff recurrence2Scalar1Main 183 = -((2002890835285665726725435305202621309061891690871252639559 * 10 ^ 70 + 5362236631868135606267045133105257958144838397098264553045294260605608) * 10 ^ 70 + 96268998113666938905022026496559509173888227008994388753243354003210)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_184 :
Polynomial.coeff recurrence2Scalar1Main 184 = -((1974994156265085183779973347090973305763176933330083030856 * 10 ^ 70 + 6517699452688933862672483804848710211481314125059005968133606503501158) * 10 ^ 70 + 4708438419540365093066215691882815820067469596721963907883808210123113)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_185 :
Polynomial.coeff recurrence2Scalar1Main 185 = (23257505776859172624239483184925134815435431166742918560997 * 10 ^ 70 + 9894982177117997711641065784749396578811039784537399485956729098033201) * 10 ^ 70 + 6161587010034607135545771140233992570131419840843839390574889540586345
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_186 :
Polynomial.coeff recurrence2Scalar1Main 186 = -((74694716289916314571613251812374150269874412478647340395054 * 10 ^ 70 + 3558331449972055883687821034959143911810574272691953277864317041517139) * 10 ^ 70 + 2557333217412198410892359087068259768811715736786694537589747001633164)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_187 :
Polynomial.coeff recurrence2Scalar1Main 187 = (113396418938311067788793745302215873510992811881867582171934 * 10 ^ 70 + 5394844961928314907777745227576214392017152047094105749785343803080944) * 10 ^ 70 + 6492390194494011927258624105614985612309851899605205894665295682658281
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_188 :
Polynomial.coeff recurrence2Scalar1Main 188 = (114925709998437481561798771392093603601548930099116095873158 * 10 ^ 70 + 3448537090915833212654614416016444499875291304737423040226164790181319) * 10 ^ 70 + 4881528962323426370058210565232532475238951514760432373651236859223493
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_189 :
Polynomial.coeff recurrence2Scalar1Main 189 = -((1271332227879790434117688979781491845389767687864795832113354 * 10 ^ 70 + 8863866487449068875484174564306468114645399983715357353104520479532923) * 10 ^ 70 + 2249373519682362896078994895287889598069542988586085779956336883027902)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_190 :
Polynomial.coeff recurrence2Scalar1Main 190 = (4104641454521958208791442700337213111815386120864490212889557 * 10 ^ 70 + 5565295864169558778589378597558343490122024822846085941273806822707511) * 10 ^ 70 + 1118531689137952129332783860297081217572690888549991948200092758525827
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_191 :
Polynomial.coeff recurrence2Scalar1Main 191 = -((6976212076975427887890114637585236110350809709704136230189174 * 10 ^ 70 + 141147257215813320839666002238665080941241530994602865063115649227380) * 10 ^ 70 + 3729828993435037535428711251357537994622463373258735792352433629791934)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_192 :
Polynomial.coeff recurrence2Scalar1Main 192 = -((1290008678902408699807928666935869017621282370453522648324499 * 10 ^ 70 + 8146056954052648787457138480625618175589487536350435332010497650482112) * 10 ^ 70 + 3170497615730066098193969762271883768166439257391320829936502352666720)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_193 :
Polynomial.coeff recurrence2Scalar1Main 193 = (52331809700451532853785635643015673308806664984473804458767938 * 10 ^ 70 + 645399183295902749313719537238792525563978927898769051394008547992931) * 10 ^ 70 + 7799683099396825082693744163516695975117105876270444639127827860146208
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_194 :
Polynomial.coeff recurrence2Scalar1Main 194 = -((194510205053656625581384091102829502293749202598387331559555597 * 10 ^ 70 + 2999333558987444040377846094823324593073034738925024841589986551232630) * 10 ^ 70 + 3171150449309529684759218191838905027648521300551903773902515005088681)