Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupB3Low

Recurrence 4 lookup certificate: B3 source coefficients, low 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_0 :
Polynomial.coeff remainder5Coefficient3 0 = 44628871650183547488
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_1 :
Polynomial.coeff remainder5Coefficient3 1 = -101240104527640512674952
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_2 :
Polynomial.coeff remainder5Coefficient3 2 = 87557480293910528383866378
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_3 :
Polynomial.coeff remainder5Coefficient3 3 = -17874654837571402443629296374
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_4 :
Polynomial.coeff remainder5Coefficient3 4 = 5792348008208369009856522675166
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_5 :
Polynomial.coeff remainder5Coefficient3 5 = -3806052411410356690277128193857762
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_6 :
Polynomial.coeff remainder5Coefficient3 6 = 794138340736874213339747440019444146
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_7 :
Polynomial.coeff remainder5Coefficient3 7 = 459572625303106389282958919799380335773
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_8 :
Polynomial.coeff remainder5Coefficient3 8 = -358577994602045914617846182412852893324183
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_9 :
Polynomial.coeff remainder5Coefficient3 9 = 117453494423525901032793741396672926492322148
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_10 :
Polynomial.coeff remainder5Coefficient3 10 = -23256833699296850816234761216087472158657143063
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_11 :
Polynomial.coeff remainder5Coefficient3 11 = 2945773668955325960286820698289656482971377267830
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_12 :
Polynomial.coeff remainder5Coefficient3 12 = -213822084719556136916781023460835071703455272203752
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_13 :
Polynomial.coeff remainder5Coefficient3 13 = 638886660829311632136262248982227233100505496765003
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_14 :
Polynomial.coeff remainder5Coefficient3 14 = 2040033871472087327222112859996188953567916500121335778
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_15 :
Polynomial.coeff remainder5Coefficient3 15 = -303356374870980680186516623408014726166869672865918546455
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_16 :
Polynomial.coeff remainder5Coefficient3 16 = 27730199851722782796550094216799884647900218900608773236702
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_17 :
Polynomial.coeff remainder5Coefficient3 17 = -1880852812837032786044553218841490043822390045096627260650327
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_18 :
Polynomial.coeff remainder5Coefficient3 18 = 100864985408863943121681035028321503095156460571072129419339276
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_19 :
Polynomial.coeff remainder5Coefficient3 19 = -4410561464911732753207669038807696428063173251376098165235630603
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_20 :
Polynomial.coeff remainder5Coefficient3 20 = 159958046781633673359015285134972040331564158001488513695799457938
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_21 :
Polynomial.coeff remainder5Coefficient3 21 = -4852920224108041789164917886602639001013879859584390128251128829788
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_22 :
Polynomial.coeff remainder5Coefficient3 22 = 123257136392501107939563763872623318895344303785687679174999064768092
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_23 :
Polynomial.coeff remainder5Coefficient3 23 = -2593243379732581424840542851652796204036169948577154626758769763893779
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_24 :
Polynomial.coeff remainder5Coefficient3 24 = 4 * 10 ^ 70 + 3639508018785041573247180859238733990704107143751221924005819018214348
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_25 :
Polynomial.coeff remainder5Coefficient3 25 = -(52 * 10 ^ 70 + 2794408701580335029475811808443136074388803142042355658886481700668681)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_26 :
Polynomial.coeff remainder5Coefficient3 26 = 191 * 10 ^ 70 + 800112660215775106529785918169646466978923319780337901262085447916480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_27 :
Polynomial.coeff remainder5Coefficient3 27 = 11141 * 10 ^ 70 + 3511849857216329474832474685406054859943744049806329572261682694130480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_28 :
Polynomial.coeff remainder5Coefficient3 28 = -(407290 * 10 ^ 70 + 3045987907383496458581635985232366476277965491894248531863059559825720)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_29 :
Polynomial.coeff remainder5Coefficient3 29 = 9217574 * 10 ^ 70 + 9135549243686721976790272765036986315615762241351172599843197969659141
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_30 :
Polynomial.coeff remainder5Coefficient3 30 = -(165739073 * 10 ^ 70 + 8393178619170115022086353822073760034466568321710302299436160939754865)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_31 :
Polynomial.coeff remainder5Coefficient3 31 = 2540769236 * 10 ^ 70 + 2737971722656249732995630127499560807923539459419138645281364863186103
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_32 :
Polynomial.coeff remainder5Coefficient3 32 = -(34270630597 * 10 ^ 70 + 5260375396576147330082376590665487935628609878541057979824300840798187)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_33 :
Polynomial.coeff remainder5Coefficient3 33 = 413968417707 * 10 ^ 70 + 768159759312506681994710158431281578805781514805631149378436838856709
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_34 :
Polynomial.coeff remainder5Coefficient3 34 = -(4529547653390 * 10 ^ 70 + 1180946419997081820169868900828037856659224689506173041399967110786179)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_35 :
Polynomial.coeff remainder5Coefficient3 35 = 45259190598688 * 10 ^ 70 + 8705858952268869282324877065553902415677684874140261754770859710778076
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_36 :
Polynomial.coeff remainder5Coefficient3 36 = -(415529713467702 * 10 ^ 70 + 2256702769604287657926372522304740296578776848683506033533823842366501)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_37 :
Polynomial.coeff remainder5Coefficient3 37 = 3522738397409662 * 10 ^ 70 + 4016765220425349130370239446390403149450876222015931131791111769436942
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_38 :
Polynomial.coeff remainder5Coefficient3 38 = -(27689309725903479 * 10 ^ 70 + 1961743517649459054498191698281766604177925978164467786718202996985242)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_39 :
Polynomial.coeff remainder5Coefficient3 39 = 202488576089517049 * 10 ^ 70 + 1696255787168471123939034187087325004894994085022988928254956506980802
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_40 :
Polynomial.coeff remainder5Coefficient3 40 = -(1381803467072592727 * 10 ^ 70 + 7086368517291335988072343009157215537630642398269828330309867435445702)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_41 :
Polynomial.coeff remainder5Coefficient3 41 = 8822474274536780436 * 10 ^ 70 + 4990974459380609890451868111985563423608624364041208087612101263072947
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_42 :
Polynomial.coeff remainder5Coefficient3 42 = -(52825521249394570211 * 10 ^ 70 + 4615331109661900485788728582253642400579556475127797217417838636669950)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_43 :
Polynomial.coeff remainder5Coefficient3 43 = 297240737775830770274 * 10 ^ 70 + 9160458132610332085770345246328111212309508165290986148828927357884739
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_44 :
Polynomial.coeff remainder5Coefficient3 44 = -(1574680488576089355221 * 10 ^ 70 + 4523281339076651529136900701325305605349286265756642418669605000989285)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_45 :
Polynomial.coeff remainder5Coefficient3 45 = 7867249852070201216064 * 10 ^ 70 + 4582835354055577965000807081833002153251072128419035711651336086330043
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_46 :
Polynomial.coeff remainder5Coefficient3 46 = -(37123957959450155191197 * 10 ^ 70 + 5760124693843893992999240140695448580657861924359895389868942142704525)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_47 :
Polynomial.coeff remainder5Coefficient3 47 = 165682260176268317782593 * 10 ^ 70 + 3301302915762501451795128919014615783043301872209447394357760640162962
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_48 :
Polynomial.coeff remainder5Coefficient3 48 = -(700195090778100769094274 * 10 ^ 70 + 8961002776286462335460067580822388325139769117933516121830207390101326)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_49 :
Polynomial.coeff remainder5Coefficient3 49 = 2805181297952191698703511 * 10 ^ 70 + 4776570915940082225965402050322675838233111360589180583551808423453981
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_50 :
Polynomial.coeff remainder5Coefficient3 50 = -(10664250381209080862072008 * 10 ^ 70 + 2326907715331445896771055055246870257405639879221159800257161159462394)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_51 :
Polynomial.coeff remainder5Coefficient3 51 = 38504475019789786704776645 * 10 ^ 70 + 8983006396996869648774868427255246670954591488729041129914535157342160
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_52 :
Polynomial.coeff remainder5Coefficient3 52 = -(132143671912190097130357614 * 10 ^ 70 + 4292946229161457166517579558328668493992549462154369996659440440454057)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_53 :
Polynomial.coeff remainder5Coefficient3 53 = 431360872159782438654316825 * 10 ^ 70 + 8036234880811649746678849258530024470712135587579214664102542225019780
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_54 :
Polynomial.coeff remainder5Coefficient3 54 = -(1340183506109571497063902606 * 10 ^ 70 + 2376382648473338818437309227430397538446428911475890408860555908029445)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_55 :
Polynomial.coeff remainder5Coefficient3 55 = 3965102563816793613007104873 * 10 ^ 70 + 7669836139003918374109012278136128989120729332211179373540528643837118
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_56 :
Polynomial.coeff remainder5Coefficient3 56 = -(11176826442697718790593752299 * 10 ^ 70 + 5434698714825192511936337469587818835461986256407366175319783321875354)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_57 :
Polynomial.coeff remainder5Coefficient3 57 = 30028626859400933284660010329 * 10 ^ 70 + 2821577589971645848195152637548155203957977694406158654881782336323996
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_58 :
Polynomial.coeff remainder5Coefficient3 58 = -(76923222386908198612469439296 * 10 ^ 70 + 3341194214874610232811023433697815611875690756115326982193355517231)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_59 :
Polynomial.coeff remainder5Coefficient3 59 = 187936418308826523724173820517 * 10 ^ 70 + 3245106368782011791923298190367214568750222911985006402781060698683424
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_60 :
Polynomial.coeff remainder5Coefficient3 60 = -(438023451097027151791482911844 * 10 ^ 70 + 7730213746101738616011029091076778232278377432590124436548815285823537)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_61 :
Polynomial.coeff remainder5Coefficient3 61 = 974077291448852087966243994640 * 10 ^ 70 + 8619478279412257834487582460082751292906198899490640198705715130289422
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_62 :
Polynomial.coeff remainder5Coefficient3 62 = -(2067048972359633442255109285324 * 10 ^ 70 + 6305738516992480214451493913560409004826797519381376076376508744007102)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_63 :
Polynomial.coeff remainder5Coefficient3 63 = 4185960399566808657599633892773 * 10 ^ 70 + 447811639384939185270759361273199707590360886771823322064469177780768
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_64 :
Polynomial.coeff remainder5Coefficient3 64 = -(8089554946889475071618186414570 * 10 ^ 70 + 1895120309868715185005122925394629156628694877375415094607516245733311)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_65 :
Polynomial.coeff remainder5Coefficient3 65 = 14917891086999057645249953472131 * 10 ^ 70 + 7182661947196199063760607425716135498471289896763515264000941677838133
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_66 :
Polynomial.coeff remainder5Coefficient3 66 = -(26246899527128897795645212887958 * 10 ^ 70 + 3583827882949268707360638022258960270588776673077786299802417875371295)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_67 :
Polynomial.coeff remainder5Coefficient3 67 = 44048603046095353377532741500233 * 10 ^ 70 + 4110620260441435799385807582797872265380934413664318372670975578709411
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_68 :
Polynomial.coeff remainder5Coefficient3 68 = -(70488758504919722125862871750294 * 10 ^ 70 + 5797899621271760029891666424743278626201206348764449607413507104102322)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_69 :
Polynomial.coeff remainder5Coefficient3 69 = 107506734088341871590558360622254 * 10 ^ 70 + 5853391154416279115576164407500622941278008186419272679752691266609818
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_70 :
Polynomial.coeff remainder5Coefficient3 70 = -(156172567192240961368311352868088 * 10 ^ 70 + 832188305485343202405222131616440113529551191027063581008026694684880)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_71 :
Polynomial.coeff remainder5Coefficient3 71 = 215905312135622316386388829973640 * 10 ^ 70 + 4150111837670667056683079682540821233822168908662523663492426956798173
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_72 :
Polynomial.coeff remainder5Coefficient3 72 = -(283746138931585440565379915717879 * 10 ^ 70 + 7009736779007018113494667782115832625249975579570903766136417339645489)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_73 :
Polynomial.coeff remainder5Coefficient3 73 = 353966701013215527976567122246798 * 10 ^ 70 + 9475444560026207689510546158924523244269220605787077959012473179569303
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_74 :
Polynomial.coeff remainder5Coefficient3 74 = -(418302556100057284066113364708798 * 10 ^ 70 + 3368134098031839614036812729567800301335034507507892651867841021289729)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_75 :
Polynomial.coeff remainder5Coefficient3 75 = 466989545386178572791198025680847 * 10 ^ 70 + 4618926056407144463538334815773833405340377379702610354691358391129612
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_76 :
Polynomial.coeff remainder5Coefficient3 76 = -(490547659350129264547771562843313 * 10 ^ 70 + 5765235804124122310591950203756087085187378185536250437642820594675614)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_77 :
Polynomial.coeff remainder5Coefficient3 77 = 481963803343730379591219664934208 * 10 ^ 70 + 797713169024014102697671774008190735681225826766876223926065977504657
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_78 :
Polynomial.coeff remainder5Coefficient3 78 = -(438685785455757082394429316503438 * 10 ^ 70 + 9971832649563398329956573298717006220741802878350499538441111088018414)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_79 :
Polynomial.coeff remainder5Coefficient3 79 = 363776410241906267150856140275008 * 10 ^ 70 + 3666959042408336993729472472236887947459308342183623692484889321248307
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_80 :
Polynomial.coeff remainder5Coefficient3 80 = -(265756197179930269188800932349881 * 10 ^ 70 + 7855889992975456826301417432471310176545788550286663062198216203431520)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_81 :
Polynomial.coeff remainder5Coefficient3 81 = 157051856645012416764023332324660 * 10 ^ 70 + 8861731037690843658743470204948967759312879879751776858305124001783265
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4B3_coeff_82 :
Polynomial.coeff remainder5Coefficient3 82 = -(51428654316374346130452468229279 * 10 ^ 70 + 5177134521289598425608709100741533805154815794406205125847464435015873)