Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupB3High

Recurrence 4 lookup certificate: B3 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.recurrence4B3_coeff_83 :
Polynomial.coeff remainder5Coefficient3 83 = -(38866524666380547875837444104940 * 10 ^ 70 + 463135121556001943361877811080921396267668670016027569207659636665257)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_84 :
Polynomial.coeff remainder5Coefficient3 84 = 105434881176286219116035112835576 * 10 ^ 70 + 4386147372602646935399683680836246740876085816326599821787753933764121
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_85 :
Polynomial.coeff remainder5Coefficient3 85 = -(144917089886819899668343951163705 * 10 ^ 70 + 5850433856894143966257138741104570758797103270625117531443555047211953)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_86 :
Polynomial.coeff remainder5Coefficient3 86 = 158843796729181183350641618062268 * 10 ^ 70 + 6025790967197498871186390511452210992568929896303793887310399367345801
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_87 :
Polynomial.coeff remainder5Coefficient3 87 = -(152380841997167014450205992970841 * 10 ^ 70 + 8832074230851428664087615385827018970423589273919066452696707891501460)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_88 :
Polynomial.coeff remainder5Coefficient3 88 = 132502910941961766778860435498979 * 10 ^ 70 + 6296153408421758870203122667828763572723809084994783100811580798174386
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_89 :
Polynomial.coeff remainder5Coefficient3 89 = -(106196957413207610240661914274181 * 10 ^ 70 + 5064720109850364858601845053482187707392993546993237957224100253696845)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_90 :
Polynomial.coeff remainder5Coefficient3 90 = 79151570986805408699120099583243 * 10 ^ 70 + 2075256976602656422516788412962736278688107634309273468718726270328490
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_91 :
Polynomial.coeff remainder5Coefficient3 91 = -(55129287473034259111582574722714 * 10 ^ 70 + 8596176377546819932522521782095089922869147652794004643231283005387920)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_92 :
Polynomial.coeff remainder5Coefficient3 92 = 35966434902340090582175075854111 * 10 ^ 70 + 5069913435799182198731971762948255036276530914310873996997115188210585
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_93 :
Polynomial.coeff remainder5Coefficient3 93 = -(21986080137314593993572124509336 * 10 ^ 70 + 9205853948079244252215688820624060220278917201136457427261272643117317)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_94 :
Polynomial.coeff remainder5Coefficient3 94 = 12569921986038285190246301295709 * 10 ^ 70 + 9458621703552866650256146646246428535862475844601595520750014961922575
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_95 :
Polynomial.coeff remainder5Coefficient3 95 = -(6687567179750649601175618559701 * 10 ^ 70 + 6668252114244857721107735725381019049825708945042015472963987458386645)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_96 :
Polynomial.coeff remainder5Coefficient3 96 = 3274945748984358533973554765119 * 10 ^ 70 + 185701735801513203052829191719772742180992793602736750837031900425450
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_97 :
Polynomial.coeff remainder5Coefficient3 97 = -(1440722250665432004726932162896 * 10 ^ 70 + 7962192300751123010066394322808273805571102485226879452623934040197532)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_98 :
Polynomial.coeff remainder5Coefficient3 98 = 534635579414320096001818351489 * 10 ^ 70 + 6913588216391918418763080550667204587086244005748260820257534215077409
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_99 :
Polynomial.coeff remainder5Coefficient3 99 = -(131314890499990449910642215431 * 10 ^ 70 + 7983970260228061013870669275419345902411243533189976469720000369779107)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_100 :
Polynomial.coeff remainder5Coefficient3 100 = -(22256513202262452421416960142 * 10 ^ 70 + 6431889941553794805633225977656116443036077263229232041502366017897699)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_101 :
Polynomial.coeff remainder5Coefficient3 101 = 63765539895758961975962646311 * 10 ^ 70 + 4489195657552337736017458289577032247764983751711953835334993304935804
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_102 :
Polynomial.coeff remainder5Coefficient3 102 = -(61736059766702977257720900041 * 10 ^ 70 + 7255389882194287992375520840483464678266365752902138633838354833933684)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_103 :
Polynomial.coeff remainder5Coefficient3 103 = 47045459646322062254384476090 * 10 ^ 70 + 2433743790701573624896685254758867494447719352162775032376198964277174
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_104 :
Polynomial.coeff remainder5Coefficient3 104 = -(31883421230393916142372931385 * 10 ^ 70 + 291191241315227264395628183421641661266666475481675126440847489171224)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_105 :
Polynomial.coeff remainder5Coefficient3 105 = 20014786803757761117594854278 * 10 ^ 70 + 8532106140057871055305950863729875067015508094831430992273683821966706
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_106 :
Polynomial.coeff remainder5Coefficient3 106 = -(11833914101911832478839446948 * 10 ^ 70 + 8612256903224192738769040110069849608597957092215826824489899315112149)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_107 :
Polynomial.coeff remainder5Coefficient3 107 = 6635998698761293632313916588 * 10 ^ 70 + 634386835836255605862448665025875994467171066670900773853088123753012
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_108 :
Polynomial.coeff remainder5Coefficient3 108 = -(3537263806839638322101889877 * 10 ^ 70 + 2018644866931270903514048036210308226195079097618305987229338945651800)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_109 :
Polynomial.coeff remainder5Coefficient3 109 = 1791951898693664225315499999 * 10 ^ 70 + 9209066654989055274430717240781249842781332932532326447028296351846681
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_110 :
Polynomial.coeff remainder5Coefficient3 110 = -(861311853462650295421391267 * 10 ^ 70 + 4560088306180548290320138300896978133850331300868575807100128208724786)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_111 :
Polynomial.coeff remainder5Coefficient3 111 = 391715821334677356994457970 * 10 ^ 70 + 558087061862455915597512523386932145946620362000162525723884758663581
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_112 :
Polynomial.coeff remainder5Coefficient3 112 = -(167908562084820451374149594 * 10 ^ 70 + 5608620202432050101733823491895275700332458918650205103665570599069909)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_113 :
Polynomial.coeff remainder5Coefficient3 113 = 67472806317180529198800521 * 10 ^ 70 + 3635744446896161362664664515263421644082910031760677475172099624374038
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_114 :
Polynomial.coeff remainder5Coefficient3 114 = -(25221732513405105672635134 * 10 ^ 70 + 7482810008088764554572586945680447609115119151309125347772054877259942)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_115 :
Polynomial.coeff remainder5Coefficient3 115 = 8666212257663366710065626 * 10 ^ 70 + 3360989125947937477347094301236868162860236572730930210981877424116017
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_116 :
Polynomial.coeff remainder5Coefficient3 116 = -(2682071204279719275428831 * 10 ^ 70 + 2554736177282735165100334008994346847894094891383993342775134787954509)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_117 :
Polynomial.coeff remainder5Coefficient3 117 = 718099623756892137411207 * 10 ^ 70 + 2338832378787989429550548553779685262606546592832324546168056808858456
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_118 :
Polynomial.coeff remainder5Coefficient3 118 = -(149754047146599061490275 * 10 ^ 70 + 9030789110887770194531983158919213357167609295166850298420880139759178)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_119 :
Polynomial.coeff remainder5Coefficient3 119 = 14066818375939978447552 * 10 ^ 70 + 7483336653041955039714876047485002154187596384476111245838011231906044
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_120 :
Polynomial.coeff remainder5Coefficient3 120 = 7153267115087379481075 * 10 ^ 70 + 3738601004821785136892398227263712734217169397486377693901635217713420
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_121 :
Polynomial.coeff remainder5Coefficient3 121 = -(5571037959944728193364 * 10 ^ 70 + 7839818693262929463154730085238906187343131443587111363057389849890604)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_122 :
Polynomial.coeff remainder5Coefficient3 122 = 2496425329652168959163 * 10 ^ 70 + 2730586219107887807749854784397869978639458792583844484768424578268574
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_123 :
Polynomial.coeff remainder5Coefficient3 123 = -(893195493581331439755 * 10 ^ 70 + 1506312348291388333427412056339945507962724153696335766498496528378212)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_124 :
Polynomial.coeff remainder5Coefficient3 124 = 279949140122051847231 * 10 ^ 70 + 6728094773313306515340519287808161963166150205503215116437248232445686
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_125 :
Polynomial.coeff remainder5Coefficient3 125 = -(82045205654896499005 * 10 ^ 70 + 5002630844393361614722555305815029189470766194637034553393481831566015)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_126 :
Polynomial.coeff remainder5Coefficient3 126 = 23919097922365774810 * 10 ^ 70 + 3632316705478465367937017332106330790966047997315844772445794376395698
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_127 :
Polynomial.coeff remainder5Coefficient3 127 = -(7087895102910589144 * 10 ^ 70 + 4077205386867391149140616205601285755369880083314353892045332094452362)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_128 :
Polynomial.coeff remainder5Coefficient3 128 = 1988211811144196534 * 10 ^ 70 + 4444227088683247192723031882873092951297742137480563920562845666892917
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_129 :
Polynomial.coeff remainder5Coefficient3 129 = -(429170244792093409 * 10 ^ 70 + 3594978665480329275182028819636344591172555247919534270529237303282461)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_130 :
Polynomial.coeff remainder5Coefficient3 130 = 16394927632172079 * 10 ^ 70 + 4123304788303407181147077219244260079596964970848652196270666501217506
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_131 :
Polynomial.coeff remainder5Coefficient3 131 = 47923566457021272 * 10 ^ 70 + 8919564065579675767190237270157057793142933814753734818123395084871501
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_132 :
Polynomial.coeff remainder5Coefficient3 132 = -(34027882878653173 * 10 ^ 70 + 5559687891473258478739168418832766435238815372726621843558034028528531)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_133 :
Polynomial.coeff remainder5Coefficient3 133 = 16734293580497187 * 10 ^ 70 + 3192460633887513726281493467513867022753847600585226996924735295029124
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_134 :
Polynomial.coeff remainder5Coefficient3 134 = -(7276315826067875 * 10 ^ 70 + 5337844594360375077406408494129592083958167958112185652274142691347588)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_135 :
Polynomial.coeff remainder5Coefficient3 135 = 3052004246526034 * 10 ^ 70 + 6285091038109868691844960508344423590935707479148947414175404196855425
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_136 :
Polynomial.coeff remainder5Coefficient3 136 = -(1252352536157476 * 10 ^ 70 + 4294614329760815953036187985899619841761358228946124415375473325316301)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_137 :
Polynomial.coeff remainder5Coefficient3 137 = 490086019343389 * 10 ^ 70 + 666563362201878453880494878598837376754885055526032164126822548355779
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_138 :
Polynomial.coeff remainder5Coefficient3 138 = -(177680969145688 * 10 ^ 70 + 1943785531615753838205815329909910410031223867315661663299633748769632)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_139 :
Polynomial.coeff remainder5Coefficient3 139 = 58672027318845 * 10 ^ 70 + 9583933738652132260962959360806876609816532021610475873984094855579144
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_140 :
Polynomial.coeff remainder5Coefficient3 140 = -(17523655908987 * 10 ^ 70 + 7808981551880645915088830573668170689051267646364616009853068412381126)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_141 :
Polynomial.coeff remainder5Coefficient3 141 = 4719695436388 * 10 ^ 70 + 9639310025966502297891576706146950088813340304074227493651028770551507
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_142 :
Polynomial.coeff remainder5Coefficient3 142 = -(1142002140033 * 10 ^ 70 + 6454920949718300868914805238703351531471563501638538982241130917012180)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_143 :
Polynomial.coeff remainder5Coefficient3 143 = 246577578629 * 10 ^ 70 + 8360843595338571701530320934762205654968001848214092633662211486208236
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_144 :
Polynomial.coeff remainder5Coefficient3 144 = -(47030080520 * 10 ^ 70 + 8114431842106427346933256177582164650114592401381382322065608472866408)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_145 :
Polynomial.coeff remainder5Coefficient3 145 = 7820287055 * 10 ^ 70 + 7193673705063847092219873265125510273993295296249092569605768787726447
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_146 :
Polynomial.coeff remainder5Coefficient3 146 = -(1115536633 * 10 ^ 70 + 1952180484080311972236737136082337622405845563655525665927588269196789)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_147 :
Polynomial.coeff remainder5Coefficient3 147 = 133781693 * 10 ^ 70 + 4470209109764542348822037942549792825924635984366536167159122902603647
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_148 :
Polynomial.coeff remainder5Coefficient3 148 = -(13131959 * 10 ^ 70 + 6370032493029726392368481496909338105613298368327001969328293681842791)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_149 :
Polynomial.coeff remainder5Coefficient3 149 = 1015604 * 10 ^ 70 + 4714784963104680389751730198818462215040446882376720092826248007019278
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_150 :
Polynomial.coeff remainder5Coefficient3 150 = -(58390 * 10 ^ 70 + 1959169823620478784665064289498459448642811587137818129067006798624831)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_151 :
Polynomial.coeff remainder5Coefficient3 151 = 2266 * 10 ^ 70 + 2063717219107911485446457576525190668901308954367462719133703628939739
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_152 :
Polynomial.coeff remainder5Coefficient3 152 = -(49 * 10 ^ 70 + 3192305225148937266252799061341011193663669472250138318183586520266448)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_153 :
Polynomial.coeff remainder5Coefficient3 153 = 3569551290947626014550370920088617484593554421017738743263080005527564
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_154 :
Polynomial.coeff remainder5Coefficient3 154 = 15364874460241919274310490770747333416206943644342775551943578689598
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_155 :
Polynomial.coeff remainder5Coefficient3 155 = -154482697540332732953226464329676070749837843645479196701309115059
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_156 :
Polynomial.coeff remainder5Coefficient3 156 = -11667054656340848662684049708286368298828614767731465825095689
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_157 :
Polynomial.coeff remainder5Coefficient3 157 = 1339932918728827906856052854523919863221616769269288116977253
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_158 :
Polynomial.coeff remainder5Coefficient3 158 = -2258019364603840472915416091506789967149902086294606087436
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_159 :
Polynomial.coeff remainder5Coefficient3 159 = 1114441137360318994499517012134430527617844825944987556
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_160 :
Polynomial.coeff remainder5Coefficient3 160 = -153773405756152491463125105370326757909641795149761
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_161 :
Polynomial.coeff remainder5Coefficient3 161 = 4932242405094780241174003775565952210999946079
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_162 :
Polynomial.coeff remainder5Coefficient3 162 = -27544084507760918430706034189549153086265
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_163 :
Polynomial.coeff remainder5Coefficient3 163 = 16735719307940309486145372463218633
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_164 :
Polynomial.coeff remainder5Coefficient3 164 = -447151549834258283177195510