Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar2ShiftPart1.Coefficients234To266

Recurrence 2 lookup certificate: Scalar2Shift 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.recurrence2Scalar2Shift_coeff_234 :
Polynomial.coeff recurrence2Scalar2Shift 234 = ((48 * 10 ^ 70 + 2962827913965204441738001666219567317871876274463657598126022907390265) * 10 ^ 70 + 4228325507692423703258496434312210842870779908511480452241313174463135) * 10 ^ 70 + 8822618747197629630089221450846338301362698919453238836795882130225162
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_235 :
Polynomial.coeff recurrence2Scalar2Shift 235 = -(((36 * 10 ^ 70 + 2190689495487898547553993397841742446260549355813899767495833555470646) * 10 ^ 70 + 2255438662295955506395230489630087629770362854344266139853695647341779) * 10 ^ 70 + 6159830212430958205332965387328957645179393088121560477028201041078707)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_236 :
Polynomial.coeff recurrence2Scalar2Shift 236 = ((20 * 10 ^ 70 + 6010266253252941148904635726743268413616435238082671175756339892389530) * 10 ^ 70 + 588795760586034099322676167261349373158733624403364961842527709648878) * 10 ^ 70 + 9746247687887126252704257534950366944620699215499268069674213661896012
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_237 :
Polynomial.coeff recurrence2Scalar2Shift 237 = -(((2 * 10 ^ 70 + 9246045897399059095618852318896129876438809197590827390277497678048309) * 10 ^ 70 + 6614978567776163825088581937738593259403337879591990988311370807252985) * 10 ^ 70 + 2343904691615547347767057109886289353524004495151013188075864552135695)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_238 :
Polynomial.coeff recurrence2Scalar2Shift 238 = -(((15 * 10 ^ 70 + 122941114894798788877071021396046095083558579569677103214018185327495) * 10 ^ 70 + 5350157152480672470110101849793445359574342417755076337042735012957221) * 10 ^ 70 + 849628554476050027605364856023632828864816053221488850508551319845589)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_239 :
Polynomial.coeff recurrence2Scalar2Shift 239 = ((31 * 10 ^ 70 + 3858421888809494486613324232295619512155046974038151311654249997290172) * 10 ^ 70 + 9372577647722527013012939313254466216831348304518412440356046991208905) * 10 ^ 70 + 5103138692793371382250468381176230086712235553860372746506428103697279
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_240 :
Polynomial.coeff recurrence2Scalar2Shift 240 = -(((44 * 10 ^ 70 + 6376390115002654768713496314733985290443342732597194420154043448242590) * 10 ^ 70 + 5404429024374801901306310022051828010954946983124356642539954428828292) * 10 ^ 70 + 1463717980521246198721095751136827342579518915942150687285790205804255)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_241 :
Polynomial.coeff recurrence2Scalar2Shift 241 = ((53 * 10 ^ 70 + 7058635175361350180945849030648275047288110065710904922239093746067700) * 10 ^ 70 + 3357137623813454306645449992188275759573278730017794292045914902998213) * 10 ^ 70 + 3042315987536898038463144777346122425694811804411936792083626186189959
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_242 :
Polynomial.coeff recurrence2Scalar2Shift 242 = -(((58 * 10 ^ 70 + 1510036327376251140569163515681145650661985163124413412653386260759354) * 10 ^ 70 + 2262370887992595835357832129209939838809659875144981511887877665063058) * 10 ^ 70 + 4428951997396214693773513451069550465839807339074210949494090374594583)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_243 :
Polynomial.coeff recurrence2Scalar2Shift 243 = ((58 * 10 ^ 70 + 1584894767227658790863341269289325003285141116989983957972891375880732) * 10 ^ 70 + 6860605727937503424618345668639522275440435140459566140236617025641166) * 10 ^ 70 + 6406405075009981528426457265746255063894723534878210252819370603458177
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_244 :
Polynomial.coeff recurrence2Scalar2Shift 244 = -(((54 * 10 ^ 70 + 4304089357797021876148075169687403562272725315516804003565278763557885) * 10 ^ 70 + 4206222861174817058489621720318896158554309611513062238028566750499401) * 10 ^ 70 + 2968827249611740100901531153609395777325740925458931948667020697754325)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_245 :
Polynomial.coeff recurrence2Scalar2Shift 245 = ((48 * 10 ^ 70 + 21732619105953940122364599892271432592321085994290384043415676851913) * 10 ^ 70 + 7732047748980429357450297228285252845199532473999790186050706444794691) * 10 ^ 70 + 9738886844371714569090433930401288171144423296186654796652546950685414
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_246 :
Polynomial.coeff recurrence2Scalar2Shift 246 = -(((40 * 10 ^ 70 + 317810926116711082879961142581124328373381458388114661474967101447268) * 10 ^ 70 + 4495886788183502668557485476236752839496482454238369687402670229033129) * 10 ^ 70 + 7850718211361120538963653449418562204580234037022107999942751438355413)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_247 :
Polynomial.coeff recurrence2Scalar2Shift 247 = ((31 * 10 ^ 70 + 6076749295505813183146786870569200735429142380123354995612980988313379) * 10 ^ 70 + 9393518053817560584652340640180902255884096458984227454954923404092530) * 10 ^ 70 + 1798688169452839111214344765908693927091252430859363887462660566225911
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_248 :
Polynomial.coeff recurrence2Scalar2Shift 248 = -(((23 * 10 ^ 70 + 6086835459845646092975590954239387139590395017201379410284940719192771) * 10 ^ 70 + 5782546402808545392024902236658362183194198405319372362452936896568532) * 10 ^ 70 + 7599725458797910033801271489668915814650429118362336943624220128370271)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_249 :
Polynomial.coeff recurrence2Scalar2Shift 249 = ((16 * 10 ^ 70 + 6314474328256077317266682372041941362249313996353358837954215977000053) * 10 ^ 70 + 2441178602412307935876369392598258509578304257340366960149613961401043) * 10 ^ 70 + 3371836281923524654322962549210100797213043960683712526460610464728062
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_250 :
Polynomial.coeff recurrence2Scalar2Shift 250 = -(((10 * 10 ^ 70 + 9828627824549486149701963195261944605109566581065176994788877118413484) * 10 ^ 70 + 3674996153446893828663972694753898790625531984231583578068208374139489) * 10 ^ 70 + 3154277891426453826051354743039905560324405162727538425119669455053522)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_251 :
Polynomial.coeff recurrence2Scalar2Shift 251 = ((6 * 10 ^ 70 + 7219871008979510213505086662747763326655953933827576876226701581620840) * 10 ^ 70 + 1423281795987172193108027504851744869841938594389142316395843052784844) * 10 ^ 70 + 6417225282550830204072361991292161538073812385328254657054127412326918
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_252 :
Polynomial.coeff recurrence2Scalar2Shift 252 = -(((3 * 10 ^ 70 + 7296954300550042501373299481379288831624076877499066961801085208932339) * 10 ^ 70 + 6055422100922595465670072018909736494358034338813947297894772478557420) * 10 ^ 70 + 6227974827135937429466095573149666726655048732217771033782439173300694)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_253 :
Polynomial.coeff recurrence2Scalar2Shift 253 = ((1 * 10 ^ 70 + 7848885883886769583070130980775502699272880485400698682945631377818524) * 10 ^ 70 + 2267073548768168704835685225143641456050899737859263601371376349389145) * 10 ^ 70 + 6975862832398219151988746282524805902120523660961826330366817798923190
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_254 :
Polynomial.coeff recurrence2Scalar2Shift 254 = -((6312301770305459578442851637688437330439525166073941787173585596013019 * 10 ^ 70 + 5064674725781192943165362067747739738344651869589431054648656555092429) * 10 ^ 70 + 4842497528055149182312964893515837630176651768248178050636747527526282)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_255 :
Polynomial.coeff recurrence2Scalar2Shift 255 = (255506465793852879611511993813218072286857349565370743806458533566380 * 10 ^ 70 + 3291942862738296113168727366691280166717468146026876336451058243375929) * 10 ^ 70 + 9949001716473500565900826735529646268306800196654613780890075364144263
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_256 :
Polynomial.coeff recurrence2Scalar2Shift 256 = (2341796344176257440915365955761500643035478445033530852623957660550082 * 10 ^ 70 + 7643358211697304369876400276781785135908801634224907523648623137945087) * 10 ^ 70 + 1552827999472881497396604853999999523287495197468108649528242216522749
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_257 :
Polynomial.coeff recurrence2Scalar2Shift 257 = -((2985464885138773705026035345829957780384117370691217714074807626208396 * 10 ^ 70 + 8947986140864625982232791447288102997838222658077907942831902521015713) * 10 ^ 70 + 9950737582014413972258120223303533352839028461597623888593301278136762)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_258 :
Polynomial.coeff recurrence2Scalar2Shift 258 = (2688329394878073578326619194496281170623274222416528761643644139255876 * 10 ^ 70 + 7463853446094363907172524664025796664876909855909341013404545861158847) * 10 ^ 70 + 8705595290620570861371839682500534691640284558742849103892526084781435
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_259 :
Polynomial.coeff recurrence2Scalar2Shift 259 = -((2060110971312770383784079461313145951045947354015574116523588982841499 * 10 ^ 70 + 3576701471306738119860373164832965848054134488222503517024887749911158) * 10 ^ 70 + 4384333548310348675467345074811113490039334315004720333124413808505513)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_260 :
Polynomial.coeff recurrence2Scalar2Shift 260 = (1419859840253737887937127792723299402643702874169276421101596325671142 * 10 ^ 70 + 9471817969395373191800104151588213794204035395033005929678238916931064) * 10 ^ 70 + 9035493899111856804970892038096331022219441971985117544454032624221347
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_261 :
Polynomial.coeff recurrence2Scalar2Shift 261 = -((900624950193395317982976310468280861340696507335073300295596730983903 * 10 ^ 70 + 3942701259104463084878728337627769672451978613963136278481035830642665) * 10 ^ 70 + 6297039465373009725265104056806966979173863055623753364272346593797505)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_262 :
Polynomial.coeff recurrence2Scalar2Shift 262 = (531401147264142943434836783412510489851410766072982544702024155092776 * 10 ^ 70 + 8588637295225962560581157425080166335336807911393127747654167587531273) * 10 ^ 70 + 2706248311266452239978360530760256871954000426551338820885854232534930
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_263 :
Polynomial.coeff recurrence2Scalar2Shift 263 = -((292952003725448832628172272851543689366298682011011097511294213513572 * 10 ^ 70 + 131526671754217837706904778839777322156158002626079365557897306803038) * 10 ^ 70 + 4892015756361626397892704042614965947895353030563388130296001799967647)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_264 :
Polynomial.coeff recurrence2Scalar2Shift 264 = (150920580440551130199955047097878107706258140745910022308530430347533 * 10 ^ 70 + 9363033958752869837498274703092293712100810087439661866303399769036142) * 10 ^ 70 + 3639548729485558579533534580954945282253694050569096037317424154862627
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_265 :
Polynomial.coeff recurrence2Scalar2Shift 265 = -((72382307710137060036792432980666829050645212783618265776723306297419 * 10 ^ 70 + 5770244255423849928431998392523851052974819389464321776889297284747928) * 10 ^ 70 + 1930849293888061121148829401236610678470442778865663156508328476293976)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Shift_coeff_266 :
Polynomial.coeff recurrence2Scalar2Shift 266 = (32025426077174270233886456060290433743208691193223241601221168369851 * 10 ^ 70 + 461956998040511591549963431763140670947456506080749731972124305964381) * 10 ^ 70 + 9327051817690650480933060640508862269294171483289567623583306361124276