Recurrence 2 lookup certificate: Scalar0Exceptional coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_17 :
Polynomial.coeff recurrence2Scalar0Exceptional 17 = 209612374313426307946070982140592077020795638985
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_18 :
Polynomial.coeff recurrence2Scalar0Exceptional 18 = -52277126010691497465575917478191008938358895298199
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_19 :
Polynomial.coeff recurrence2Scalar0Exceptional 19 = 8805879311219840232385681613488948016673578494840122
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_20 :
Polynomial.coeff recurrence2Scalar0Exceptional 20 = -1135726015262387796842575054645517055852497256862351007
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_21 :
Polynomial.coeff recurrence2Scalar0Exceptional 21 = 103600755085640996389090553616425237352073287427134470143
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_22 :
Polynomial.coeff recurrence2Scalar0Exceptional 22 = -4490880968489304429409162624318884839521007404361398513972
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_23 :
Polynomial.coeff recurrence2Scalar0Exceptional 23 = -386115562701539525686276830345659497273368170156883495335397
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_24 :
Polynomial.coeff recurrence2Scalar0Exceptional 24 = 100549835533793813507164400050824793136449703852559684153893117
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_25 :
Polynomial.coeff recurrence2Scalar0Exceptional 25 = -11035158908934234104966143214656709773729206148083100259558467465
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_26 :
Polynomial.coeff recurrence2Scalar0Exceptional 26 = 744901736715026387567349432996593659242884431583082050978924416746
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_27 :
Polynomial.coeff recurrence2Scalar0Exceptional 27 = -24610275543656074008441298594425745945956930910004113878336690192065
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_28 :
Polynomial.coeff recurrence2Scalar0Exceptional 28 = -1067404451848261438706112497218228432224655216854555032790785736623930
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_29 :
Polynomial.coeff recurrence2Scalar0Exceptional 29 = 22 * 10 ^ 70 + 7673908314146694996295581349342060919367917772217783582850863479347679
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_30 :
Polynomial.coeff recurrence2Scalar0Exceptional 30 = -(1926 * 10 ^ 70 + 7747257216924354751147028365501884602921216463160395197786686811826043)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_31 :
Polynomial.coeff recurrence2Scalar0Exceptional 31 = 111842 * 10 ^ 70 + 2383135276709768463935187184406308901183301049957696398314772712612352
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_32 :
Polynomial.coeff recurrence2Scalar0Exceptional 32 = -(4882809 * 10 ^ 70 + 9052006221761899484130666710773802007689658560732060948582766775659711)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_33 :
Polynomial.coeff recurrence2Scalar0Exceptional 33 = 163276362 * 10 ^ 70 + 6300411817405597187236388888706498158823405735286122311539627051575853
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_34 :
Polynomial.coeff recurrence2Scalar0Exceptional 34 = -(4136234309 * 10 ^ 70 + 1039195732398111058002198782755967967543228895957761173979227672179253)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_35 :
Polynomial.coeff recurrence2Scalar0Exceptional 35 = 79601993501 * 10 ^ 70 + 3087246593067753012240169123453064904040749916612467200293178828941047
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_36 :
Polynomial.coeff recurrence2Scalar0Exceptional 36 = -(1518195084825 * 10 ^ 70 + 8812240571868462356584717308789630452155297628592922261191031687211686)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_37 :
Polynomial.coeff recurrence2Scalar0Exceptional 37 = 57786605508570 * 10 ^ 70 + 2588237512489506567108735089567634623678726778770459693715398393642168
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_38 :
Polynomial.coeff recurrence2Scalar0Exceptional 38 = -(3027255031009804 * 10 ^ 70 + 8199637740426195712420076973895345166281506221680596075105789992640141)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_39 :
Polynomial.coeff recurrence2Scalar0Exceptional 39 = 127920123799398956 * 10 ^ 70 + 9980365466750498242345895531750898714468389182381648290666040278824137
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_40 :
Polynomial.coeff recurrence2Scalar0Exceptional 40 = -(4130625270299475736 * 10 ^ 70 + 5558614887244539406725911907209875674322674954086822642087540651517886)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_41 :
Polynomial.coeff recurrence2Scalar0Exceptional 41 = 106515411682457957088 * 10 ^ 70 + 385749802693013550743768773663646235753896636118687173437930753269705
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_42 :
Polynomial.coeff recurrence2Scalar0Exceptional 42 = -(2368528197306259966229 * 10 ^ 70 + 5429945800241236075461000292233202312366774981999199302326612669932456)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_43 :
Polynomial.coeff recurrence2Scalar0Exceptional 43 = 51943811759050239588500 * 10 ^ 70 + 279365764521474408496199036266737036685621161471921481492515579917693
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_44 :
Polynomial.coeff recurrence2Scalar0Exceptional 44 = -(1298746785932773869108802 * 10 ^ 70 + 7204373158098071440352972107380571937754856704345660534969759392648141)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_45 :
Polynomial.coeff recurrence2Scalar0Exceptional 45 = 37048850232232114598331394 * 10 ^ 70 + 2638964305871133191093258653668653802473753478263141287723718606630713
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_46 :
Polynomial.coeff recurrence2Scalar0Exceptional 46 = -(1079586125565787712536338014 * 10 ^ 70 + 802197497293342940352842986735727534095496246058587252051579489437012)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_47 :
Polynomial.coeff recurrence2Scalar0Exceptional 47 = 29965874381460649227775264120 * 10 ^ 70 + 8342122822822796719356016046788392539521310979757896972199637889103227
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_48 :
Polynomial.coeff recurrence2Scalar0Exceptional 48 = -(782424154159467425090312085352 * 10 ^ 70 + 1473190560394734387598646297831982085340275501556904958753700642677178)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_49 :
Polynomial.coeff recurrence2Scalar0Exceptional 49 = 19346726309076880317960144913499 * 10 ^ 70 + 5833867836342045790762174339641510458979612336352937312950332719491151
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_50 :
Polynomial.coeff recurrence2Scalar0Exceptional 50 = -(454926622044824834644788999420042 * 10 ^ 70 + 1622834197436082383755700599536020184208729696628999996374521403104814)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_51 :
Polynomial.coeff recurrence2Scalar0Exceptional 51 = 10158885609107450585370171452189794 * 10 ^ 70 + 9571069129130258970954403162167901348498175520377605618553804419734821
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_52 :
Polynomial.coeff recurrence2Scalar0Exceptional 52 = -(214949766478060782110562557122553117 * 10 ^ 70 + 6690156212305180238567329140740437215037616080186060147268482962817614)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_53 :
Polynomial.coeff recurrence2Scalar0Exceptional 53 = 4311365162991463139766873017402624056 * 10 ^ 70 + 4193335738141172961854884620614703888538511365683261207868397872990184
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_54 :
Polynomial.coeff recurrence2Scalar0Exceptional 54 = -(82235093059694851369352734320019202488 * 10 ^ 70 + 1107919956278914852736841803416682044685123736869922933039443243169739)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_55 :
Polynomial.coeff recurrence2Scalar0Exceptional 55 = 1497332985236493458240647980679041305446 * 10 ^ 70 + 4075995320804572346244905142933226056020659331963924763646088454638875
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_56 :
Polynomial.coeff recurrence2Scalar0Exceptional 56 = -(26093593735945943013017250471918957452017 * 10 ^ 70 + 1583137342499081488304009900676972259848232143428681736634775333937927)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_57 :
Polynomial.coeff recurrence2Scalar0Exceptional 57 = 435656018648405426395140078689560701107765 * 10 ^ 70 + 850786675046856181043729735378445765414788454178304039706080104846054
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_58 :
Polynomial.coeff recurrence2Scalar0Exceptional 58 = -(6969782614172348294709391197849213968443916 * 10 ^ 70 + 1734129635308949387681112144654085943001530349219681560689810680347109)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_59 :
Polynomial.coeff recurrence2Scalar0Exceptional 59 = 106871666166197603064653239026238460044744104 * 10 ^ 70 + 5630522662061416755253902041904686178475249703656324637814057610979716
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_60 :
Polynomial.coeff recurrence2Scalar0Exceptional 60 = -(1571706340958533788027317292233497409692834859 * 10 ^ 70 + 6616780397382101209894822567081247849899763230835587503148514261936953)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_61 :
Polynomial.coeff recurrence2Scalar0Exceptional 61 = 22190265921079002035712262221102170660949112121 * 10 ^ 70 + 7503525871894952497362368297632930272531554595000559035892921629627308
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_62 :
Polynomial.coeff recurrence2Scalar0Exceptional 62 = -(301042259591096638061049963458291386101422057878 * 10 ^ 70 + 2584385893135196501853109015546743194097167999849566154901392766721154)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_63 :
Polynomial.coeff recurrence2Scalar0Exceptional 63 = 3927083896531825008848936571506303331312560600134 * 10 ^ 70 + 1020644492132618903953617918520735753838504461699791381389347891780718
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_64 :
Polynomial.coeff recurrence2Scalar0Exceptional 64 = -(49288716323665777719769965216139379253030414459756 * 10 ^ 70 + 3113885084380172792184690069148506887710049897745683423269835309816291)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_65 :
Polynomial.coeff recurrence2Scalar0Exceptional 65 = 595575787789779229646919386702658411683748335845466 * 10 ^ 70 + 4672860176768397740150912872287003339838493900104543706848443702673936
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_66 :
Polynomial.coeff recurrence2Scalar0Exceptional 66 = -(6933571342071093606585222049260921799020503226341145 * 10 ^ 70 + 866706891140751853863371971297896084940378118782920365362703838812317)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_67 :
Polynomial.coeff recurrence2Scalar0Exceptional 67 = 77826903350517268253247176845554380247582462654483179 * 10 ^ 70 + 3406043383253428102092704638393527308986892484368343137733675571036888
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_68 :
Polynomial.coeff recurrence2Scalar0Exceptional 68 = -(842822587757616720928829902139709888474910023162419469 * 10 ^ 70 + 4761345623521887327958879260759759854533040895084210903055815361172262)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_69 :
Polynomial.coeff recurrence2Scalar0Exceptional 69 = 8810635996106929419293368885073489891283730383580986137 * 10 ^ 70 + 1956320483052557761887139926131811264537896592465135298795080008122783
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_70 :
Polynomial.coeff recurrence2Scalar0Exceptional 70 = -(88952099597043509806514019698439522635021261846399346903 * 10 ^ 70 + 3006310904478639710807934341253932976676608861959638782758950569008066)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_71 :
Polynomial.coeff recurrence2Scalar0Exceptional 71 = 867790161118323151957321786072332938291123779314537006137 * 10 ^ 70 + 130082331899306877512960665533355944646514433761260057302892419929440
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_72 :
Polynomial.coeff recurrence2Scalar0Exceptional 72 = -(8185382498111655803345415806718671483285544342696096763695 * 10 ^ 70 + 2176829440953214810335743315637195905315834392503613946368952512314732)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_73 :
Polynomial.coeff recurrence2Scalar0Exceptional 73 = 74693640499504375990666947810994507384680176345767868116245 * 10 ^ 70 + 2202747786245130486033270404616519772891555812059600243827973243685907
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_74 :
Polynomial.coeff recurrence2Scalar0Exceptional 74 = -(659740906259793370061394046523915726748575587316517753064065 * 10 ^ 70 + 7810472497407775611507692734047785428652935516744729785889099800349042)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_75 :
Polynomial.coeff recurrence2Scalar0Exceptional 75 = 5642883370220084682419955996770932059764964401444523568910235 * 10 ^ 70 + 6206414808528233650785172153341868917668278112312822338242089982427926
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_76 :
Polynomial.coeff recurrence2Scalar0Exceptional 76 = -(46757535208206887968740336056466944638539881542941965719004435 * 10 ^ 70 + 1853103767921777260753946206425049702093901429957365736005180741697200)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_77 :
Polynomial.coeff recurrence2Scalar0Exceptional 77 = 375513940713235741679576122374419039307232387863287757022692785 * 10 ^ 70 + 1228888827160591090839504978144889370462986192652068226917445372907041
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_78 :
Polynomial.coeff recurrence2Scalar0Exceptional 78 = -(2924418120229870129555540818159684523353894987043887750728625282 * 10 ^ 70 + 2633689476318703962085069621217278070822367018626503043638224060042403)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_79 :
Polynomial.coeff recurrence2Scalar0Exceptional 79 = 22095066631575384558344888017377666903231664465020450400052556359 * 10 ^ 70 + 6632491488671734839102885251228702002149739982872253736589033543021454
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_80 :
Polynomial.coeff recurrence2Scalar0Exceptional 80 = -(162018593797041701513360982827570391041434175423130536191252886930 * 10 ^ 70 + 5836655676607591644008282771254177462558285957895529265713152535061012)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_81 :
Polynomial.coeff recurrence2Scalar0Exceptional 81 = 1153442617848806628014250492361975475064896204282263283498202300047 * 10 ^ 70 + 9739590301476209208885493137155987960473163066711638917024164739081002
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_82 :
Polynomial.coeff recurrence2Scalar0Exceptional 82 = -(7975271998740645849078870635097444785734339874234549370073253733322 * 10 ^ 70 + 8434593985082585283971448833370448614544542248619588664867926665632698)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_83 :
Polynomial.coeff recurrence2Scalar0Exceptional 83 = 53579700800750337608723840649419869417356389476484158358833005461905 * 10 ^ 70 + 2923807735854907960433840015524453973964911640028509680856110723234723
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_84 :
Polynomial.coeff recurrence2Scalar0Exceptional 84 = -(349912802763281854422318321522243158196607594891332956867472082400151 * 10 ^ 70 + 31276479518231178389634598150200636638320827400353174503023459334633)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_85 :
Polynomial.coeff recurrence2Scalar0Exceptional 85 = 2222245841493897171467341832997798426849370028484528045178394619293651 * 10 ^ 70 + 3540551805791241703728823672545832570768879113915879568409087334452722
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_86 :
Polynomial.coeff recurrence2Scalar0Exceptional 86 = -((1 * 10 ^ 70 + 3728078322121480417733504142417970782875154395474026497583039289686432) * 10 ^ 70 + 2110746970097693867538901608443481227828033835125050565140430186404867)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_87 :
Polynomial.coeff recurrence2Scalar0Exceptional 87 = (8 * 10 ^ 70 + 2509189480135759224593121562498640582543199067324579667182732878136241) * 10 ^ 70 + 188601638123294823335141291563732063465131203709496743012009133349845
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_88 :
Polynomial.coeff recurrence2Scalar0Exceptional 88 = -((48 * 10 ^ 70 + 2617087060456592098969612559808173542306177514776635069711249174403364) * 10 ^ 70 + 821498552358418727235729728806111600558879510711732016030163555763847)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_89 :
Polynomial.coeff recurrence2Scalar0Exceptional 89 = (274 * 10 ^ 70 + 8633234368343039040516392437711832532779784987022513671734275940944317) * 10 ^ 70 + 9353973026980340743881617569251385274402388974742568956369951927220361
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Exceptional_coeff_90 :
Polynomial.coeff recurrence2Scalar0Exceptional 90 = -((1524 * 10 ^ 70 + 9844821370637777331880063429312845256184155174701318412334857316514284) * 10 ^ 70 + 9622684958110837454120538392338260398627467921335258201305454533683007)