Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupB0High

Recurrence 4 lookup certificate: B0 source coefficients, high half #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_89 :
Polynomial.coeff remainder5Coefficient0 89 = 243147735284975507376814912992944908 * 10 ^ 70 + 8557715862645962643237058026038259758378686283339453029262466594182846
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_90 :
Polynomial.coeff remainder5Coefficient0 90 = -(196570064417209207402024567782066485 * 10 ^ 70 + 8111306650775855388461585614486476679213270750269932217180976499493967)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_91 :
Polynomial.coeff remainder5Coefficient0 91 = 153159057587230801202148153108656317 * 10 ^ 70 + 2371274006398823507317617931899219375721860364188342865194779142944771
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_92 :
Polynomial.coeff remainder5Coefficient0 92 = -(114954094916425396884730080291259003 * 10 ^ 70 + 2792712530220514662369310636128444097904970134081365575234313593152034)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_93 :
Polynomial.coeff remainder5Coefficient0 93 = 83036932908714184707010020885642192 * 10 ^ 70 + 8180836420984302120492298484868299040857209327288072906445955283454234
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_94 :
Polynomial.coeff remainder5Coefficient0 94 = -(57648068286239957301060107129095405 * 10 ^ 70 + 7035210123962120614755934021842561134490370038735923881214201333468459)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_95 :
Polynomial.coeff remainder5Coefficient0 95 = 38389762264277030046579145302915826 * 10 ^ 70 + 6681065842038195951380479463027602637776250928807350202649955707771321
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_96 :
Polynomial.coeff remainder5Coefficient0 96 = -(24457109512611868896120714431405630 * 10 ^ 70 + 6213559414400152043678921729199868713918134083833479972128498362382139)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_97 :
Polynomial.coeff remainder5Coefficient0 97 = 14852510626318070971062415596573688 * 10 ^ 70 + 6052146140850048889052129686785818056474144078353406580514072726697656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_98 :
Polynomial.coeff remainder5Coefficient0 98 = -(8556666442269158542558965486346253 * 10 ^ 70 + 230385368537477086586246254262546027335658736017785069761755587786893)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_99 :
Polynomial.coeff remainder5Coefficient0 99 = 4645396585339123012614011814285997 * 10 ^ 70 + 4449249604938466792344043431391243197675021868939705326673292109206927
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_100 :
Polynomial.coeff remainder5Coefficient0 100 = -(2353733508847175662626747827303171 * 10 ^ 70 + 7208968374930526935172732079770057668347536457970980205070256731535507)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_101 :
Polynomial.coeff remainder5Coefficient0 101 = 1096400251195361400687322073877634 * 10 ^ 70 + 2187822014915311889885588065678227428990509937482551342006991423807757
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_102 :
Polynomial.coeff remainder5Coefficient0 102 = -(457417378843535249802960581365541 * 10 ^ 70 + 3749588542164142283616094506616877596267244894223507590051238437445642)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_103 :
Polynomial.coeff remainder5Coefficient0 103 = 161983040533764105986659116397817 * 10 ^ 70 + 2751583295579569863183358137912290665706498709369211644210932496200687
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_104 :
Polynomial.coeff remainder5Coefficient0 104 = -(41845421165489106026092352796684 * 10 ^ 70 + 8597459227611041110905029128701503198432737703891170201816556514751186)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_105 :
Polynomial.coeff remainder5Coefficient0 105 = 2159391006824730258889566808068 * 10 ^ 70 + 5302122669599958645441666054294363715553449188196563257461324658206009
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_106 :
Polynomial.coeff remainder5Coefficient0 106 = 5696934172940541909492250700915 * 10 ^ 70 + 7373672361709008357828642295050743274493503998843202954909200069833600
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_107 :
Polynomial.coeff remainder5Coefficient0 107 = -(3863636548224382591159830846335 * 10 ^ 70 + 5550978757712434009339348008476559615591525269150040422651695833175372)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_108 :
Polynomial.coeff remainder5Coefficient0 108 = 841169725366383847040162135903 * 10 ^ 70 + 9511785654292213986225019770864666863336955780064885234603825355291909
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_109 :
Polynomial.coeff remainder5Coefficient0 109 = 1024161288242507256645800178189 * 10 ^ 70 + 3390729301498229185917056961900451246816906096164091827440421611503911
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_110 :
Polynomial.coeff remainder5Coefficient0 110 = -(1670368045689599111114273818286 * 10 ^ 70 + 9391503879636949963052931115318987632564808474664005623971586409273665)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_111 :
Polynomial.coeff remainder5Coefficient0 111 = 1593997083119938781403534683931 * 10 ^ 70 + 8496918812958137121736647966491670155137472242564124000747565932613095
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_112 :
Polynomial.coeff remainder5Coefficient0 112 = -(1234288876313796264416859699911 * 10 ^ 70 + 8461886589969575162032870965001679247256338208875450009791135827275439)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_113 :
Polynomial.coeff remainder5Coefficient0 113 = 844578931664838150766039177732 * 10 ^ 70 + 6112705147119230080226986792298173541085891999262694215541791777493960
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_114 :
Polynomial.coeff remainder5Coefficient0 114 = -(529484751881035101822712075718 * 10 ^ 70 + 5784914426773869240849284914099962252426850401793369926017668116409019)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_115 :
Polynomial.coeff remainder5Coefficient0 115 = 309812870731337635597895601898 * 10 ^ 70 + 5084253551032465766806105318652391809344922883339956226243279068962493
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_116 :
Polynomial.coeff remainder5Coefficient0 116 = -(170927936886847447825651158008 * 10 ^ 70 + 8023500933175430472055517414721674730006278031403976084303550370938652)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_117 :
Polynomial.coeff remainder5Coefficient0 117 = 89415540521749414159018107725 * 10 ^ 70 + 3439400542409004623976051472163064015715535602220001649552470347502198
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_118 :
Polynomial.coeff remainder5Coefficient0 118 = -(44469171990311416289235491650 * 10 ^ 70 + 3957417586821878164850538327027222721028245692085029329095873882667009)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_119 :
Polynomial.coeff remainder5Coefficient0 119 = 21040807759889349771785685457 * 10 ^ 70 + 5353533538699886952713033174688695610426419692270826974193161873519428
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_120 :
Polynomial.coeff remainder5Coefficient0 120 = -(9465088171831752309947675701 * 10 ^ 70 + 2781917262888451990194361349099395133088053597550710049900965460678000)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_121 :
Polynomial.coeff remainder5Coefficient0 121 = 4040860868032843815326194946 * 10 ^ 70 + 9735108119713053817123270770854259983089440422377134083102682718225267
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_122 :
Polynomial.coeff remainder5Coefficient0 122 = -(1632776998959620086454938713 * 10 ^ 70 + 7474316416771531471138480497502003118761635555894063087977592702343781)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_123 :
Polynomial.coeff remainder5Coefficient0 123 = 622135469841639913279685672 * 10 ^ 70 + 5947542732221817158107068829798138411939810685592715849411844263491525
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_124 :
Polynomial.coeff remainder5Coefficient0 124 = -(222459478398654489789662170 * 10 ^ 70 + 1830764086318134137208598825965633817770289233964116192749411487584429)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_125 :
Polynomial.coeff remainder5Coefficient0 125 = 74167272409662596251154948 * 10 ^ 70 + 3208446313540233721311060330738107009945446501460931979925055335285557
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_126 :
Polynomial.coeff remainder5Coefficient0 126 = -(22841616050653819348824538 * 10 ^ 70 + 7595500405439137082878496696109210434146581132849047361836296048184862)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_127 :
Polynomial.coeff remainder5Coefficient0 127 = 6400242853473661187606654 * 10 ^ 70 + 9716422262958750080723348537930461833671267119919693862555190552421355
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_128 :
Polynomial.coeff remainder5Coefficient0 128 = -(1583070870835501147948935 * 10 ^ 70 + 8592912452557020375826155502969265289417072883460140889990102360925485)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_129 :
Polynomial.coeff remainder5Coefficient0 129 = 318938877647812508699132 * 10 ^ 70 + 8004679114249331820660016855086132223663268043506072381836184953049583
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_130 :
Polynomial.coeff remainder5Coefficient0 130 = -(35730162632940079321348 * 10 ^ 70 + 2585678697441586119655958272918934512938400235136469418215558070204793)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_131 :
Polynomial.coeff remainder5Coefficient0 131 = -(10216470526272953616320 * 10 ^ 70 + 6793447503767788393313174732067631709404023188160824359004238341882141)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_132 :
Polynomial.coeff remainder5Coefficient0 132 = 9959358253138980130578 * 10 ^ 70 + 8921495409047217195552076528779598528081702773167860193156349723852519
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_133 :
Polynomial.coeff remainder5Coefficient0 133 = -(5094005008172515223000 * 10 ^ 70 + 9574589833856924154510024863213111905795250544582483418243732103658939)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_134 :
Polynomial.coeff remainder5Coefficient0 134 = 2067174673303288754986 * 10 ^ 70 + 97274479399497094285627069204995388661921159320586796119303064478406
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_135 :
Polynomial.coeff remainder5Coefficient0 135 = -(698548542985301428710 * 10 ^ 70 + 2543802896846559642250219231629421114088915228277206866055150921255061)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_136 :
Polynomial.coeff remainder5Coefficient0 136 = 189609607354891277970 * 10 ^ 70 + 9021722112687325878665062607500270209148314517536557820562268162353329
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_137 :
Polynomial.coeff remainder5Coefficient0 137 = -(36147732930624206529 * 10 ^ 70 + 6021266816670478006740168810929175548945650703891366221910023974900107)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_138 :
Polynomial.coeff remainder5Coefficient0 138 = 2358553686222011319 * 10 ^ 70 + 6860303659011575325798060235920015615413218859640181824460191336757715
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_139 :
Polynomial.coeff remainder5Coefficient0 139 = 971192652277583301 * 10 ^ 70 + 2216238527911636326615615977682935761547525621855824932413501544007498
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_140 :
Polynomial.coeff remainder5Coefficient0 140 = 21645448536587636 * 10 ^ 70 + 5123264619246104505909241490866124199263892612581024937573032839223221
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_141 :
Polynomial.coeff remainder5Coefficient0 141 = -(442416726729687242 * 10 ^ 70 + 8992292561498011467221786421491281082008860919300615479577452585124148)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_142 :
Polynomial.coeff remainder5Coefficient0 142 = 352270911252513566 * 10 ^ 70 + 3616914779812836977095880332182724665602888362541493986677173879556301
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_143 :
Polynomial.coeff remainder5Coefficient0 143 = -(182747877787643959 * 10 ^ 70 + 4131715304858009066110465093977803156127460024064469225093569350908056)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_144 :
Polynomial.coeff remainder5Coefficient0 144 = 76030172293771624 * 10 ^ 70 + 3590606200115923192542927966514113742434932207480199020690712351709619
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_145 :
Polynomial.coeff remainder5Coefficient0 145 = -(27607862729546024 * 10 ^ 70 + 8842397958076327167088243213394559264310404135340648549545264449299360)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_146 :
Polynomial.coeff remainder5Coefficient0 146 = 9162807715100615 * 10 ^ 70 + 6612953693441551507746556849210950951578476463755901946137357595939196
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_147 :
Polynomial.coeff remainder5Coefficient0 147 = -(2835834934193267 * 10 ^ 70 + 4011416952528692266692170626886786853529965041213933902793321059324753)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_148 :
Polynomial.coeff remainder5Coefficient0 148 = 816923273050565 * 10 ^ 70 + 7210958019345291153317207561399895363901393129376243042063776397201872
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_149 :
Polynomial.coeff remainder5Coefficient0 149 = -(215830066128311 * 10 ^ 70 + 6421695095790720903406199805953987456387271219038782543375231190979905)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_150 :
Polynomial.coeff remainder5Coefficient0 150 = 51409809174318 * 10 ^ 70 + 507119370595627147283610374118237365879410321627366296475086060366249
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_151 :
Polynomial.coeff remainder5Coefficient0 151 = -(10899974796293 * 10 ^ 70 + 4966705983469305583762388362397722295363297434176946085816051297808553)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_152 :
Polynomial.coeff remainder5Coefficient0 152 = 2044532623099 * 10 ^ 70 + 463417226636951143015099389660107335721027252813200151097809632433810
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_153 :
Polynomial.coeff remainder5Coefficient0 153 = -(339645745982 * 10 ^ 70 + 240830011722431724203760747022910402314210109607347885206914802144674)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_154 :
Polynomial.coeff remainder5Coefficient0 154 = 50391159002 * 10 ^ 70 + 5259039850681847668682838031682438707803970728124337943070617416765458
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_155 :
Polynomial.coeff remainder5Coefficient0 155 = -(6772520759 * 10 ^ 70 + 1569508501889556651033790379855854667996664790494874744940898033690106)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_156 :
Polynomial.coeff remainder5Coefficient0 156 = 835639066 * 10 ^ 70 + 8446787866317617510745858970068897208187307841239549973097918076325983
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_157 :
Polynomial.coeff remainder5Coefficient0 157 = -(94316617 * 10 ^ 70 + 5986102626254233917143732839769472888377957425525506595001360476058166)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_158 :
Polynomial.coeff remainder5Coefficient0 158 = 9311295 * 10 ^ 70 + 3159070155810858163197306597951494675483482975524395305832381858106517
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_159 :
Polynomial.coeff remainder5Coefficient0 159 = -(711257 * 10 ^ 70 + 5381760457338263627442336783044560967834790600989907984264990130153667)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_160 :
Polynomial.coeff remainder5Coefficient0 160 = 27997 * 10 ^ 70 + 7683558938809548202635556624522589400986871333307419679496074685498330
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_161 :
Polynomial.coeff remainder5Coefficient0 161 = 1685 * 10 ^ 70 + 3087028750081903031846109477894234011225120776616170221669113503157825
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_162 :
Polynomial.coeff remainder5Coefficient0 162 = -(357 * 10 ^ 70 + 938561128905602994101094906208763892603307388238154958514349705039372)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_163 :
Polynomial.coeff remainder5Coefficient0 163 = 24 * 10 ^ 70 + 5330041988896958633548850969285021398045305333097909439213858212950283
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_164 :
Polynomial.coeff remainder5Coefficient0 164 = -7249778412873998133748802006845370228676119425865786497080138061596134
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_165 :
Polynomial.coeff remainder5Coefficient0 165 = 52956952622783827709881861482560071963290333685460121885825744846323
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_166 :
Polynomial.coeff remainder5Coefficient0 166 = 280152685655969885879173634551080225175486884028181547038251690722
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_167 :
Polynomial.coeff remainder5Coefficient0 167 = -2031690952404327765609612130635720034174061933756701558852622761
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_168 :
Polynomial.coeff remainder5Coefficient0 168 = -1458928063823863028050875425433121845305555066201276383078993
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_169 :
Polynomial.coeff remainder5Coefficient0 169 = 17431834505586844323129159562726344394790113806316568604074
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_170 :
Polynomial.coeff remainder5Coefficient0 170 = -22878977253084650022265554947451972454998443751804602608
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_171 :
Polynomial.coeff remainder5Coefficient0 171 = 8465739853890267008832801209206747768551353802553124
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_172 :
Polynomial.coeff remainder5Coefficient0 172 = -805368785374396620874539479169423728718837961557
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_173 :
Polynomial.coeff remainder5Coefficient0 173 = 15842754036030934147022086546074136452896574
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_174 :
Polynomial.coeff remainder5Coefficient0 174 = -45305433673927959040925527740176360349
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_175 :
Polynomial.coeff remainder5Coefficient0 175 = 10459335688262185635633707671032
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B0_coeff_176 :
Polynomial.coeff remainder5Coefficient0 176 = -65860748014005733131201