Recurrence 2 lookup certificate: Scalar4Shift 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.recurrence2Scalar4Shift_coeff_233 :
Polynomial.coeff recurrence2Scalar4Shift 233 = -((3697747303609449161532725258324405666646636145865784684046834031899062 * 10 ^ 70 + 6888248251788118160756442031184312638822198640916631618146659960042227) * 10 ^ 70 + 2562649836309418278402536346623624248606042399148817165426514663550310)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_234 :
Polynomial.coeff recurrence2Scalar4Shift 234 = (1617778337640174904446982413317664108607222304868168542326605029687526 * 10 ^ 70 + 6655003814863823557787413531154869832876527326321473934344460324393163) * 10 ^ 70 + 1531145190881708278605988891041505288232487546625685548561148308909305
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_235 :
Polynomial.coeff recurrence2Scalar4Shift 235 = (623892504992805310106264766458853722492877611500174805188734121453171 * 10 ^ 70 + 8903756195786656804319181364941398237196128194198568826030898984102694) * 10 ^ 70 + 4093192585299647352121527581574404918935520996326523520885889934630273
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_236 :
Polynomial.coeff recurrence2Scalar4Shift 236 = -((2793056919492907278413648533146895412940998170847781714575048760675947 * 10 ^ 70 + 5971111672218581950235451943718298523453722552806644378652949901305699) * 10 ^ 70 + 952271237934818598930571094391511973465713671116221070281806693418752)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_237 :
Polynomial.coeff recurrence2Scalar4Shift 237 = (4669803872888036657193476984330319075051224137703334272110192864203077 * 10 ^ 70 + 1282947399598724042767707440618796212573304873814305465720762686121601) * 10 ^ 70 + 6796142605671457666918661751352710651426267573682815581035301582754233
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_238 :
Polynomial.coeff recurrence2Scalar4Shift 238 = -((6083394620445621334897961448076223020632233041805410998508482434846919 * 10 ^ 70 + 7674435048505426836800996038009157698326904944373162900702745871338387) * 10 ^ 70 + 9953259068786768281283422294670078926989138470042567649205714181796266)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_239 :
Polynomial.coeff recurrence2Scalar4Shift 239 = (6936115794764979082196733855796736506792311175652772004086203563455491 * 10 ^ 70 + 9313636485713303035564251657509883621868160126535666998186893133410794) * 10 ^ 70 + 5052297229352095477933953824223150699161042856670871229307124990782589
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_240 :
Polynomial.coeff recurrence2Scalar4Shift 240 = -((7211810530134946576142359670241258735207025631360745135026624996606513 * 10 ^ 70 + 6782083768740868143877751779961135828864899287900629303336549528535151) * 10 ^ 70 + 6223809662203501672425406407946270264757755459281612052738366358510189)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_241 :
Polynomial.coeff recurrence2Scalar4Shift 241 = (6968734765322294017876488448427882148341879564234391883337045800951229 * 10 ^ 70 + 2591567704575504824090652298546030449343443941442635482489123714773957) * 10 ^ 70 + 6429613137871434469654390563052472810528691751442240542712853619397100
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_242 :
Polynomial.coeff recurrence2Scalar4Shift 242 = -((6320051536946651878113244444361130792257664894275470291497730077169447 * 10 ^ 70 + 8865057090195039149310801151560295971346151668810232194037441699777670) * 10 ^ 70 + 3842336844720836466824117227111696064540019481501097776339371962769736)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_243 :
Polynomial.coeff recurrence2Scalar4Shift 243 = (5407668294477552313890529832213886968740128684632824086404765188631400 * 10 ^ 70 + 6382383022472690558750186355515712092072489249048147919609886260764187) * 10 ^ 70 + 3024871379905234711691334149206341523159365262405301917705029813076201
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_244 :
Polynomial.coeff recurrence2Scalar4Shift 244 = -((4375748235168519679297056414088234321664793184468494027101956504822491 * 10 ^ 70 + 7444910737503297273827187851901653331718153668771311911761342002691821) * 10 ^ 70 + 7099761437780204381169629511534106428646801566771949618494935210697188)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_245 :
Polynomial.coeff recurrence2Scalar4Shift 245 = (3349185292993493076651949087063991262375896557468091114904083350959814 * 10 ^ 70 + 1638287729866925071297635243296832027310455619094835237259719812739842) * 10 ^ 70 + 3449172674587722900142142071220169576899618181535587547596901379483555
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_246 :
Polynomial.coeff recurrence2Scalar4Shift 246 = -((2420193377265609822663959497858989628786796832289216779553160813932439 * 10 ^ 70 + 8754130604829891573466321393812408327412831839878213991659736125481702) * 10 ^ 70 + 7052777164692693004258201976782703991411901403208638877909483703423301)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_247 :
Polynomial.coeff recurrence2Scalar4Shift 247 = (1643705176954451554961503921166710916386446558598464789435722314243458 * 10 ^ 70 + 6165674042939729244964274377795728581727476506205085549780188604803491) * 10 ^ 70 + 4042272527921055016545121438310529315782494447794040438063732308447669
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_248 :
Polynomial.coeff recurrence2Scalar4Shift 248 = -((1040215824936643627809959633039104910278611448997776236006039204911144 * 10 ^ 70 + 4494628489891964021684459260134847866072777944576579835278811549354455) * 10 ^ 70 + 8194861509542852822249189028798469129455859223499514461828305599219115)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_249 :
Polynomial.coeff recurrence2Scalar4Shift 249 = (603481820133818388090236254296395875435940379680338142839949701363291 * 10 ^ 70 + 8030524059170329627176339127664905508010125112197110950990461139442131) * 10 ^ 70 + 5412564904709923650726139077274528981985805356033927533925289893821995
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_250 :
Polynomial.coeff recurrence2Scalar4Shift 250 = -((310195089701854530568316478356282733931617701101166571319196315922315 * 10 ^ 70 + 66566303656996349258705701969884993856466530760894290300499159564632) * 10 ^ 70 + 7603594592304814242236077179444489790908397439499487082287553865508308)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_251 :
Polynomial.coeff recurrence2Scalar4Shift 251 = (129211211096792149119263164352966477268388008649791686827782031184934 * 10 ^ 70 + 8105713076062411713906394695626970400256374644566385613210656808261337) * 10 ^ 70 + 948918829327654990544058482364969624873644529508190476281454322376407
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_252 :
Polynomial.coeff recurrence2Scalar4Shift 252 = -((28782611092067639630255459975749708315044002226001559045528331943740 * 10 ^ 70 + 9624022910754497006181774325573973121076267425905215468495024966193544) * 10 ^ 70 + 133077166095719907762917235609676051071042859232305938245960082184143)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_253 :
Polynomial.coeff recurrence2Scalar4Shift 253 = -((18814640466712922354264348352739952636653664986644888230749208597075 * 10 ^ 70 + 4005674114508972714690631155253958332955519243786682243568736431136285) * 10 ^ 70 + 1603555724416994555901141041305431585956180705579953167539804520349527)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_254 :
Polynomial.coeff recurrence2Scalar4Shift 254 = (35121167818444049785977884810302953209477488960520546486810744493591 * 10 ^ 70 + 5291854326051415854563233546044958759557836173715546774356573080185047) * 10 ^ 70 + 7323261771843607266691289244811836905624848323056192140625755263107363
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_255 :
Polynomial.coeff recurrence2Scalar4Shift 255 = -((35216690520587175725169262199791863344853858419550028626239579726436 * 10 ^ 70 + 6932293263362076008696948734490792655735840844315106915576529666103643) * 10 ^ 70 + 8311624471301841205082119669850758992002395803256258578524785619220668)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_256 :
Polynomial.coeff recurrence2Scalar4Shift 256 = (28594023766893776893768287977512387780447946489475180231283611932112 * 10 ^ 70 + 7919329677702085357391999299593916864857955753038802100699940719185820) * 10 ^ 70 + 5297899108881110777291380886369485085449916544293972362912336754785976
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_257 :
Polynomial.coeff recurrence2Scalar4Shift 257 = -((20527999506137011547938767427341497190267582816620660816376425826164 * 10 ^ 70 + 6665102083092308531725805744822041585030159714931422458728034571541631) * 10 ^ 70 + 3215838948957849770506715254122882948470348692310223644260169919045483)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_258 :
Polynomial.coeff recurrence2Scalar4Shift 258 = (13469369689880399989408827605337794338340523453155545922646819093682 * 10 ^ 70 + 1514168361194981141224559762745361799664132849411761338517132804280690) * 10 ^ 70 + 2857363178465317348323963574929206834731609551240402468617457382491065
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_259 :
Polynomial.coeff recurrence2Scalar4Shift 259 = -((8201495501531809691395886363695795132132391907237661379230947963782 * 10 ^ 70 + 5210762217214707594994900291725201981093785374502754859575796922550951) * 10 ^ 70 + 1688446718280263844036623194603147435940546787453314659762259336068710)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_260 :
Polynomial.coeff recurrence2Scalar4Shift 260 = (4668093530264469285183162778508173408685794227924646002767055572148 * 10 ^ 70 + 8293907846289568563972397937041119504201982554715734257482924842559185) * 10 ^ 70 + 9090575798121864259727997615312815118829704375468330906543512919115267
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_261 :
Polynomial.coeff recurrence2Scalar4Shift 261 = -((2490389748468634223920912434891651861807796534828584214065245294008 * 10 ^ 70 + 9028443131785673522473871052624971252275078860712378872368957745431785) * 10 ^ 70 + 8185869199471422974032661589444843328797534929749161210821513628539613)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_262 :
Polynomial.coeff recurrence2Scalar4Shift 262 = (1244433318854504717186422819102962260011003861736763880878183686666 * 10 ^ 70 + 9181548440635540008556220176359419054122887334572029486551671659476946) * 10 ^ 70 + 4093933044356516595422983611126298928310368341220404397098512374348219
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Shift_coeff_263 :
Polynomial.coeff recurrence2Scalar4Shift 263 = -((579970965651524778057913769909767029807651321701882028599941645054 * 10 ^ 70 + 1826497761766359644115860787101773782424495147826846585859686891769415) * 10 ^ 70 + 6047091109856650934812851290676564629613459471381599830374724918052193)