Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupC4Low

Recurrence 2 lookup certificate: C4 source coefficients, low 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.recurrence2C4_coeff_0 :
Polynomial.coeff remainder4Coefficient4 0 = -384736
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_1 :
Polynomial.coeff remainder4Coefficient4 1 = 556020644
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_2 :
Polynomial.coeff remainder4Coefficient4 2 = 860860911458
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_3 :
Polynomial.coeff remainder4Coefficient4 3 = -987926129188182
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_4 :
Polynomial.coeff remainder4Coefficient4 4 = 140675585138572631
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_5 :
Polynomial.coeff remainder4Coefficient4 5 = 20151219772032322722
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_6 :
Polynomial.coeff remainder4Coefficient4 6 = -2438654708488280028551
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_7 :
Polynomial.coeff remainder4Coefficient4 7 = -553594068115153391367507
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_8 :
Polynomial.coeff remainder4Coefficient4 8 = 250410476581740108401049598
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_9 :
Polynomial.coeff remainder4Coefficient4 9 = -81352128705906514960143558313
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_10 :
Polynomial.coeff remainder4Coefficient4 10 = 20259837629907699206396766838382
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_11 :
Polynomial.coeff remainder4Coefficient4 11 = -3915823094088946880177830648985549
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_12 :
Polynomial.coeff remainder4Coefficient4 12 = 609222704994768969809439283247736730
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_13 :
Polynomial.coeff remainder4Coefficient4 13 = -78019593595669326978467154188316895773
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_14 :
Polynomial.coeff remainder4Coefficient4 14 = 8358933071370862864202832960999674154190
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_15 :
Polynomial.coeff remainder4Coefficient4 15 = -759305252792864792433701417611944011339664
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_16 :
Polynomial.coeff remainder4Coefficient4 16 = 59135356874047274919093183023644990176958476
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_17 :
Polynomial.coeff remainder4Coefficient4 17 = -3986415948365885401007649546959463265647367604
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_18 :
Polynomial.coeff remainder4Coefficient4 18 = 234548062879281292593247267168296247595866904685
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_19 :
Polynomial.coeff remainder4Coefficient4 19 = -12133524745625283729717569456466532112506261960103
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_20 :
Polynomial.coeff remainder4Coefficient4 20 = 555521874147057891042828740360306050857986744757232
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_21 :
Polynomial.coeff remainder4Coefficient4 21 = -22643651908146602027659245862682130140162172631007072
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_22 :
Polynomial.coeff remainder4Coefficient4 22 = 826147545813881830538254359649742630432773948279396433
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_23 :
Polynomial.coeff remainder4Coefficient4 23 = -27112274718196394885972448403258543727069845245422232830
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_24 :
Polynomial.coeff remainder4Coefficient4 24 = 803945236426458360854932137167489557430696893798142028543
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_25 :
Polynomial.coeff remainder4Coefficient4 25 = -21629157518737420483674560023201587716100636682098169625936
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_26 :
Polynomial.coeff remainder4Coefficient4 26 = 529991947620463645574003008043512019857708150709628587283563
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_27 :
Polynomial.coeff remainder4Coefficient4 27 = -11870193405757571851594786880528523288659666673869140466403093
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_28 :
Polynomial.coeff remainder4Coefficient4 28 = 243802724226128588316838162848955966904405137961048691693306934
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_29 :
Polynomial.coeff remainder4Coefficient4 29 = -4606241927433366204370312450758512982358834085100377992982461734
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_30 :
Polynomial.coeff remainder4Coefficient4 30 = 80283932389129692368636065087460391814795439138607761311750108190
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_31 :
Polynomial.coeff remainder4Coefficient4 31 = -1294343677823700308666563326187316069946451188904251807215487403418
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_32 :
Polynomial.coeff remainder4Coefficient4 32 = 19350899117018021095469345400462618167083980859107511636263763358237
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_33 :
Polynomial.coeff remainder4Coefficient4 33 = -268910057122057305478250620090368706296404789129515628047162552163536
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_34 :
Polynomial.coeff remainder4Coefficient4 34 = 3481198797781684209070956684317895949047772854944209220912459640612329
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_35 :
Polynomial.coeff remainder4Coefficient4 35 = -(4 * 10 ^ 70 + 2069816978636529880430425659826320304601335396317106026328309534193026)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_36 :
Polynomial.coeff remainder4Coefficient4 36 = 47 * 10 ^ 70 + 5536130370315163552446002986249228242808138662942641834887666547654304
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_37 :
Polynomial.coeff remainder4Coefficient4 37 = -(503 * 10 ^ 70 + 6970915915898173269949493334079766361445291771051351145502574069211145)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_38 :
Polynomial.coeff remainder4Coefficient4 38 = 5008 * 10 ^ 70 + 2348421387596190178569233681934397183215388035789187533245771462352539
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_39 :
Polynomial.coeff remainder4Coefficient4 39 = -(46821 * 10 ^ 70 + 2584523497335007892118489726882105576133270819749688213003003912056483)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_40 :
Polynomial.coeff remainder4Coefficient4 40 = 412210 * 10 ^ 70 + 3629419870780469374736944838899145583746380813717256349694644740010618
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_41 :
Polynomial.coeff remainder4Coefficient4 41 = -(3422547 * 10 ^ 70 + 5555055146385175787376660432902320860046826454458801815006411542101577)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_42 :
Polynomial.coeff remainder4Coefficient4 42 = 26837227 * 10 ^ 70 + 1167758742429686980912016990705175949893958474499170804116771530635570
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_43 :
Polynomial.coeff remainder4Coefficient4 43 = -(199000342 * 10 ^ 70 + 1107239130615134314538521896054539121648499404799450119805927590087804)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_44 :
Polynomial.coeff remainder4Coefficient4 44 = 1397134386 * 10 ^ 70 + 8839114119078308667636063634342480538807532753824602470515720842262314
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_45 :
Polynomial.coeff remainder4Coefficient4 45 = -(9298275190 * 10 ^ 70 + 5602499132277471137544688363989743544134612336130865600148734706931650)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_46 :
Polynomial.coeff remainder4Coefficient4 46 = 58726129299 * 10 ^ 70 + 1394987425914761020935733723801606879887569186278747467651786943915114
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_47 :
Polynomial.coeff remainder4Coefficient4 47 = -(352358577014 * 10 ^ 70 + 1247329120526219461357067305299134329561334952556181129397913795136213)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_48 :
Polynomial.coeff remainder4Coefficient4 48 = 2010475502705 * 10 ^ 70 + 6326565649084614686255826952163620860493547554005842552351912479797296
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_49 :
Polynomial.coeff remainder4Coefficient4 49 = -(10919098153848 * 10 ^ 70 + 3088849006561933257781743687354273382887569192273107570735936318719108)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_50 :
Polynomial.coeff remainder4Coefficient4 50 = 56499059595260 * 10 ^ 70 + 312472701746886715272396274414098116356132902531490282719742507162890
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_51 :
Polynomial.coeff remainder4Coefficient4 51 = -(278762623395781 * 10 ^ 70 + 1125038440162610369815678780453126310544486688132175893404019857607163)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_52 :
Polynomial.coeff remainder4Coefficient4 52 = 1312563151471495 * 10 ^ 70 + 4709493237340617472289138587068063357178774075995854126095530823876944
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_53 :
Polynomial.coeff remainder4Coefficient4 53 = -(5902469173874552 * 10 ^ 70 + 3730060243736670659024274806605956595630888317433610193208711919217756)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_54 :
Polynomial.coeff remainder4Coefficient4 54 = 25368429550744922 * 10 ^ 70 + 2962422593388561023338289253930948841536496796464962494164370673492379
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_55 :
Polynomial.coeff remainder4Coefficient4 55 = -(104280252790568816 * 10 ^ 70 + 3659089962353617150948759230586230270578392890381004328775234865826359)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_56 :
Polynomial.coeff remainder4Coefficient4 56 = 410247670716327812 * 10 ^ 70 + 3226978922889689751135255189417253951304064421564428774643224685708198
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_57 :
Polynomial.coeff remainder4Coefficient4 57 = -(1545603185594230299 * 10 ^ 70 + 7777425665469858131214901928667178565055273229443110579427226750399534)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_58 :
Polynomial.coeff remainder4Coefficient4 58 = 5579766659762988852 * 10 ^ 70 + 5787495498228005445559530777811029662766103844299341402120193682014928
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_59 :
Polynomial.coeff remainder4Coefficient4 59 = -(19312799571455915326 * 10 ^ 70 + 1095428853027805894466671764872070568018416002980709564247880332800749)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_60 :
Polynomial.coeff remainder4Coefficient4 60 = 64123598648046353957 * 10 ^ 70 + 7566359916704976215263096295825163666350783796849645613928417290951667
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_61 :
Polynomial.coeff remainder4Coefficient4 61 = -(204340352448663420486 * 10 ^ 70 + 9060419829768585239228056752117392860892913253723345712130726749091264)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_62 :
Polynomial.coeff remainder4Coefficient4 62 = 625262653027928975232 * 10 ^ 70 + 9586258464150814772698687533048191760731560429491669466687835985439656
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_63 :
Polynomial.coeff remainder4Coefficient4 63 = -(1837977925247326697725 * 10 ^ 70 + 6378624767047399592218473981087341215139760649451028790387149647667046)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_64 :
Polynomial.coeff remainder4Coefficient4 64 = 5192472387558946323185 * 10 ^ 70 + 5484436147838198290473502338160926051848179076417134326405674943731919
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_65 :
Polynomial.coeff remainder4Coefficient4 65 = -(14103944046598663618951 * 10 ^ 70 + 9917730513354002508552127528782873838613482135539718630971389013991269)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_66 :
Polynomial.coeff remainder4Coefficient4 66 = 36847321266820794210476 * 10 ^ 70 + 9230249844726472640311402363998608128506467693836164857220459949323907
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_67 :
Polynomial.coeff remainder4Coefficient4 67 = -(92624781888426856985814 * 10 ^ 70 + 9893143880278236732011122471547671096826986561165764563795194444860851)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_68 :
Polynomial.coeff remainder4Coefficient4 68 = 224105337115893695498012 * 10 ^ 70 + 7143120318489014495622948269508240459934559670554185019172046759429088
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_69 :
Polynomial.coeff remainder4Coefficient4 69 = -(522059322098771308955969 * 10 ^ 70 + 7801768007439033769966637723136736146770053442272402277630651519310698)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_70 :
Polynomial.coeff remainder4Coefficient4 70 = 1171279470717965460664504 * 10 ^ 70 + 267015796420237791812663679799033587508382564218194404891740601452651
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_71 :
Polynomial.coeff remainder4Coefficient4 71 = -(2531607099224979223840810 * 10 ^ 70 + 8029045983027480503737953087159739436778866876725554564860683183055928)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_72 :
Polynomial.coeff remainder4Coefficient4 72 = 5272799021302746891817609 * 10 ^ 70 + 5632624327288438787582079842192948990184434419265842411403608671843023
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_73 :
Polynomial.coeff remainder4Coefficient4 73 = -(10585259667018243301605326 * 10 ^ 70 + 7359017397246505655118297497023876002011665835779618948011892352387125)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_74 :
Polynomial.coeff remainder4Coefficient4 74 = 20486882055607355997675195 * 10 ^ 70 + 9701828573769151958448956131227286748294613918110651312348269341008785
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_75 :
Polynomial.coeff remainder4Coefficient4 75 = -(38234513163566550179918934 * 10 ^ 70 + 9025950628455738998153058628668889069057607486296695895832740908053035)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_76 :
Polynomial.coeff remainder4Coefficient4 76 = 68821592199388266185196598 * 10 ^ 70 + 5123981910678457676707561291517953866616426430942848000707797088761643
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_77 :
Polynomial.coeff remainder4Coefficient4 77 = -(119497938719427052145339967 * 10 ^ 70 + 4669143043602120433076946477214705233405569342296659478708314682688878)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_78 :
Polynomial.coeff remainder4Coefficient4 78 = 200185629245334498267012310 * 10 ^ 70 + 3833768920471961844183171669125055162880931413089027162548905515384973
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_79 :
Polynomial.coeff remainder4Coefficient4 79 = -(323597900651783888512377146 * 10 ^ 70 + 8395913972185322271704500364188194359393680985910201638655046968318410)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_80 :
Polynomial.coeff remainder4Coefficient4 80 = 504819078964217346364173275 * 10 ^ 70 + 9064130092406132445737175093074842067579619038044864533626593236554200
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_81 :
Polynomial.coeff remainder4Coefficient4 81 = -(760104996931713523061946357 * 10 ^ 70 + 5969210529300953962792129617132662136262721002621981321878704231469229)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_82 :
Polynomial.coeff remainder4Coefficient4 82 = 1104748260958109602736940995 * 10 ^ 70 + 8680996677193045406160091908871631726687233251891689132614334991561734
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_83 :
Polynomial.coeff remainder4Coefficient4 83 = -(1550039894944171929426261531 * 10 ^ 70 + 6922173335598232377465026718183709162075842253383821768399749009009028)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_84 :
Polynomial.coeff remainder4Coefficient4 84 = 2099635817601882465375984245 * 10 ^ 70 + 5316433486781299060471962915079466864800455381412556420691958695643974
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_85 :
Polynomial.coeff remainder4Coefficient4 85 = -(2745947733558828359543759758 * 10 ^ 70 + 7062504235179655080848080626927271249782722825257201026517768606743628)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_86 :
Polynomial.coeff remainder4Coefficient4 86 = 3467427494206627981915665376 * 10 ^ 70 + 4544177015132306643490744959233081469936091890337657894520392761516530
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_87 :
Polynomial.coeff remainder4Coefficient4 87 = -(4227688755108568721315539096 * 10 ^ 70 + 976769010667191094651315444291129518532673081146259616139665313163006)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_88 :
Polynomial.coeff remainder4Coefficient4 88 = 4977220428643708569238497389 * 10 ^ 70 + 9974932646606808412843799254079918694385412678777989546279227028588664
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2C4_coeff_89 :
Polynomial.coeff remainder4Coefficient4 89 = -(5657972995158680361051411580 * 10 ^ 70 + 1644863562327990884794512726787286056575044192210484323842853898965418)