Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupB2High

Recurrence 2 lookup certificate: B2 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.recurrence2B2_coeff_74 :
Polynomial.coeff remainder3Coefficient2 74 = -(48380612 * 10 ^ 70 + 5807736123651960748029311842457560255736945738204410330523200568952260)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_75 :
Polynomial.coeff remainder3Coefficient2 75 = 52399116 * 10 ^ 70 + 7770562787171192347484713869695582412439151555427480508975751709820955
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_76 :
Polynomial.coeff remainder3Coefficient2 76 = 107166672 * 10 ^ 70 + 5440105407199975529011841541270732034051950886271738620517456422152047
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_77 :
Polynomial.coeff remainder3Coefficient2 77 = -(841933614 * 10 ^ 70 + 5195486471546444844639582432741639081154222478481994343614119951929873)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_78 :
Polynomial.coeff remainder3Coefficient2 78 = 3107058602 * 10 ^ 70 + 8575533537966814752107681158725330531559295349324840267049168204212129
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_79 :
Polynomial.coeff remainder3Coefficient2 79 = -(8773527652 * 10 ^ 70 + 1230941836863563003666073305004776276234976737873801757428613106117883)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_80 :
Polynomial.coeff remainder3Coefficient2 80 = 20998415085 * 10 ^ 70 + 9919551749454457773268112361470632809987902168684317820942572855625756
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_81 :
Polynomial.coeff remainder3Coefficient2 81 = -(44381318534 * 10 ^ 70 + 9991263522080593701675830045279755086470509237212549004952614599067836)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_82 :
Polynomial.coeff remainder3Coefficient2 82 = 84619708782 * 10 ^ 70 + 5182960830123775269160213699923146932640641182513694132981459534339840
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_83 :
Polynomial.coeff remainder3Coefficient2 83 = -(147421930894 * 10 ^ 70 + 7706039837280037719223729477628176833507078285282096993655663177966866)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_84 :
Polynomial.coeff remainder3Coefficient2 84 = 236666170457 * 10 ^ 70 + 6729176633787840805536982086739222216021383988402340329014646659614868
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_85 :
Polynomial.coeff remainder3Coefficient2 85 = -(352179049125 * 10 ^ 70 + 2965591377213287177576881910496550810869277228925378637784289444061185)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_86 :
Polynomial.coeff remainder3Coefficient2 86 = 487895867774 * 10 ^ 70 + 8172552623183993860838773198665262867925026377947262128756387467729355
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_87 :
Polynomial.coeff remainder3Coefficient2 87 = -(631322318862 * 10 ^ 70 + 7745520386782674434168398018887582965950172115711016381395623210886699)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_88 :
Polynomial.coeff remainder3Coefficient2 88 = 764957633435 * 10 ^ 70 + 5262921675886643795518394449271592980846168144490216083156286725179810
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_89 :
Polynomial.coeff remainder3Coefficient2 89 = -(869666016974 * 10 ^ 70 + 9247515814676320711805214435858709310274527504992268040365030782945048)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_90 :
Polynomial.coeff remainder3Coefficient2 90 = 929150495622 * 10 ^ 70 + 607486260275725415665031661219655566975464158435763998554034408554480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_91 :
Polynomial.coeff remainder3Coefficient2 91 = -(934095095674 * 10 ^ 70 + 9192471828259133872859662088215163160511923113444117696730716028180224)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_92 :
Polynomial.coeff remainder3Coefficient2 92 = 884531678433 * 10 ^ 70 + 8692901094669615449669766070519250450292523084406166617076303714279159
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_93 :
Polynomial.coeff remainder3Coefficient2 93 = -(789611610993 * 10 ^ 70 + 1799268872997803709586067011435150914429479252792584491414568389724059)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_94 :
Polynomial.coeff remainder3Coefficient2 94 = 664942061269 * 10 ^ 70 + 9135338432189625888500495771915866405248649841807175754422661512499891
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_95 :
Polynomial.coeff remainder3Coefficient2 95 = -(528520392947 * 10 ^ 70 + 4997527372842096920042464534806899023615255895802918082215516192145774)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_96 :
Polynomial.coeff remainder3Coefficient2 96 = 396680569299 * 10 ^ 70 + 8762561882331514688247223528604670263469644760728124408662115906623395
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_97 :
Polynomial.coeff remainder3Coefficient2 97 = -(281241665706 * 10 ^ 70 + 8056806788737292238830452277858362790864191804878612755888438156771610)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_98 :
Polynomial.coeff remainder3Coefficient2 98 = 188411640372 * 10 ^ 70 + 9949346202045504220818498858162623313256366101561117504765028790497700
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_99 :
Polynomial.coeff remainder3Coefficient2 99 = -(119297396032 * 10 ^ 70 + 8987229107472584980350730821716258482294929301075098159562646123036503)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_100 :
Polynomial.coeff remainder3Coefficient2 100 = 71405769206 * 10 ^ 70 + 6029865589604113091419977440487922673444086032763502423849396950279416
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_101 :
Polynomial.coeff remainder3Coefficient2 101 = -(40408775765 * 10 ^ 70 + 4661435721225872224038364036391109826680982581666362786191551875430469)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_102 :
Polynomial.coeff remainder3Coefficient2 102 = 21621758313 * 10 ^ 70 + 9531823907399361439529348444260659020277621502005525504665463291009353
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_103 :
Polynomial.coeff remainder3Coefficient2 103 = -(10938910645 * 10 ^ 70 + 154930183536201085638951475155070008832443978726648528516074363443685)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_104 :
Polynomial.coeff remainder3Coefficient2 104 = 5231979799 * 10 ^ 70 + 311232815505304664380859811791115565533207489647734100299043137156138
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_105 :
Polynomial.coeff remainder3Coefficient2 105 = -(2365008918 * 10 ^ 70 + 1178437391060507335313003191109706233441566022648438160414367711400991)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_106 :
Polynomial.coeff remainder3Coefficient2 106 = 1009804210 * 10 ^ 70 + 3165083692827076657670753797373804887895297423411954063969389581151368
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_107 :
Polynomial.coeff remainder3Coefficient2 107 = -(406917943 * 10 ^ 70 + 6436706490024028444350089890583884145684810998237906683449509258064080)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_108 :
Polynomial.coeff remainder3Coefficient2 108 = 154560466 * 10 ^ 70 + 4960767846161518367809748171508613227035233358423742338650833991643039
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_109 :
Polynomial.coeff remainder3Coefficient2 109 = -(55240906 * 10 ^ 70 + 2841964684254711041690876799138153832260128413836379376381369612946193)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_110 :
Polynomial.coeff remainder3Coefficient2 110 = 18535256 * 10 ^ 70 + 904930368592815932380381576355851551316029050931749931300118178605900
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_111 :
Polynomial.coeff remainder3Coefficient2 111 = -(5821512 * 10 ^ 70 + 8906236695980483756084115106517291392548948680941089857212726578660303)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_112 :
Polynomial.coeff remainder3Coefficient2 112 = 1705206 * 10 ^ 70 + 1253393681835039412989419604298863122129266837879542283424132438243727
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_113 :
Polynomial.coeff remainder3Coefficient2 113 = -(463720 * 10 ^ 70 + 6126802533542607293997760943851314674432049460003414568296716125593865)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_114 :
Polynomial.coeff remainder3Coefficient2 114 = 116429 * 10 ^ 70 + 9929306790927109332300531702373845252155692296120035775140746680497093
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_115 :
Polynomial.coeff remainder3Coefficient2 115 = -(26805 * 10 ^ 70 + 3974593728480433715158939486055239104791127235534198899486263968825702)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_116 :
Polynomial.coeff remainder3Coefficient2 116 = 5609 * 10 ^ 70 + 8287185765485529213994082243262581584135657387543776870949233940638251
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_117 :
Polynomial.coeff remainder3Coefficient2 117 = -(1054 * 10 ^ 70 + 9445995579726899352496198976701305591064216596749616103919801888854209)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_118 :
Polynomial.coeff remainder3Coefficient2 118 = 175 * 10 ^ 70 + 3428219162708042442929021584283905383289737567132038310659234492806248
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_119 :
Polynomial.coeff remainder3Coefficient2 119 = -(25 * 10 ^ 70 + 847183531193488012110421608822055089562893084198397695106008999443863)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_120 :
Polynomial.coeff remainder3Coefficient2 120 = 2 * 10 ^ 70 + 9347117917665943159179787044301639136720281522779247972409835369510261
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_121 :
Polynomial.coeff remainder3Coefficient2 121 = -2446500681235254820503020803171739951147113076143029101929298950265299
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_122 :
Polynomial.coeff remainder3Coefficient2 122 = 53313951655807229356091123970641619108721066463092394318897182995114
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_123 :
Polynomial.coeff remainder3Coefficient2 123 = 27739334662807329564267888375865993661995166764506857963097879248305
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_124 :
Polynomial.coeff remainder3Coefficient2 124 = -6572864111312376157183801082731963573243496346867076686409667113807
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_125 :
Polynomial.coeff remainder3Coefficient2 125 = 934681107860434837000953261878398686818274156008261289171673950871
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_126 :
Polynomial.coeff remainder3Coefficient2 126 = -98631113392338475087316148944972009748966393538867971507679983646
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_127 :
Polynomial.coeff remainder3Coefficient2 127 = 8070972681488537876096594324281849283907104357091359639643098128
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_128 :
Polynomial.coeff remainder3Coefficient2 128 = -513168991194838191484932827443203554829686858690826486174294323
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_129 :
Polynomial.coeff remainder3Coefficient2 129 = 24887956221358816884567392188078705225648221779419059150477356
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_130 :
Polynomial.coeff remainder3Coefficient2 130 = -888796707805812581979468384138402810818976447442320188418243
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_131 :
Polynomial.coeff remainder3Coefficient2 131 = 22102615787889023365940715477631828559349160837530666583016
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_132 :
Polynomial.coeff remainder3Coefficient2 132 = -349215718451208953719573869056996934238274938879200054710
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_133 :
Polynomial.coeff remainder3Coefficient2 133 = 2892042315176818529738807354915088841226469430894035494
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_134 :
Polynomial.coeff remainder3Coefficient2 134 = -3984496954486262589407169793306672512000502855155540
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_135 :
Polynomial.coeff remainder3Coefficient2 135 = -103101870016126360746150005911720546492853629670543
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_136 :
Polynomial.coeff remainder3Coefficient2 136 = 536387544838059037062928334334550440874733909731
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_137 :
Polynomial.coeff remainder3Coefficient2 137 = 100574681677421432279576674671370954256997612
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_138 :
Polynomial.coeff remainder3Coefficient2 138 = -5622196839184792936462092408424956837028696
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_139 :
Polynomial.coeff remainder3Coefficient2 139 = 12655902568973616262798152588184214229432
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_140 :
Polynomial.coeff remainder3Coefficient2 140 = -10521605408537418559835170422339834894
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_141 :
Polynomial.coeff remainder3Coefficient2 141 = 3222330311416572061294843994497685
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_142 :
Polynomial.coeff remainder3Coefficient2 142 = -301677638040674755667972554263
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_143 :
Polynomial.coeff remainder3Coefficient2 143 = 6373118709373069341699962
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_144 :
Polynomial.coeff remainder3Coefficient2 144 = -18614232357864327257
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_145 :
Polynomial.coeff remainder3Coefficient2 145 = 2740936995785
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2B2_coeff_146 :
Polynomial.coeff remainder3Coefficient2 146 = -2406