Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar0ExceptionalPart0.Coefficients0To90

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_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)