Recurrence 4 lookup certificate: A4Square coefficient convolution #
This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_222 :
Polynomial.coeff recurrence4A4Square 222 = (1182072006687935465273941831606394974808607223739731 * 10 ^ 70 + 6315552030352667797067171269214974984286911680281254850565786724981345) * 10 ^ 70 + 281232893484383628358475326456128867352810113039991328703961788380016
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_223 :
Polynomial.coeff recurrence4A4Square 223 = -((587387178885558399965447221522601124297839214080941 * 10 ^ 70 + 1347968242824723279138538497288698516495064153226996167043948391607072) * 10 ^ 70 + 8681459426811015069191051951419074011383585885151862310623956332715322)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_224 :
Polynomial.coeff recurrence4A4Square 224 = (286295299152058462086833904026207012627376354149729 * 10 ^ 70 + 6857826224996465823614014020804227595347206566651258642192142733167126) * 10 ^ 70 + 2758626364785829528547888737304577479639227952576160355387941559789989
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_225 :
Polynomial.coeff recurrence4A4Square 225 = -((136865015299054938140534792459627288506058948285054 * 10 ^ 70 + 4294997364099332501541645378962925576719285251592204849839987029957172) * 10 ^ 70 + 9390851864849431178149512409250361582500685954921573713311943394948086)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_226 :
Polynomial.coeff recurrence4A4Square 226 = (64170934622251829717605530121159757866281281710084 * 10 ^ 70 + 4833189201077549808735850632565546437225617081772128005400818131125379) * 10 ^ 70 + 5415261745342372382960152330503058896686600323588515281189409125536025
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_227 :
Polynomial.coeff recurrence4A4Square 227 = -((29507292774058430489856995898889332098228077405321 * 10 ^ 70 + 4059870618158936542519553811707327881534606341428212621359012222647246) * 10 ^ 70 + 6477885878814018626197833334104619592245268432188161223588775033771966)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_228 :
Polynomial.coeff recurrence4A4Square 228 = (13305705396080431929332769657755651930643357127411 * 10 ^ 70 + 7195797961797084156292218224126032861824257596762122244961492406834019) * 10 ^ 70 + 9982670702463847841885452658763462193221039799023873642671770289372383
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_229 :
Polynomial.coeff recurrence4A4Square 229 = -((5883368513232270154410150391060792563042276943545 * 10 ^ 70 + 7105090254961782204815255730662422728633950181291567541723001243928726) * 10 ^ 70 + 4322758309480132793433623676315308420152725622704849945234842118656258)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_230 :
Polynomial.coeff recurrence4A4Square 230 = (2550565669300601948233770722524602336400276486864 * 10 ^ 70 + 1070356695309750931057907913194849040296785415908485681511384610110583) * 10 ^ 70 + 9950711738336692454579166698660832038423509325594143254846800926649234
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_231 :
Polynomial.coeff recurrence4A4Square 231 = -((1083871866237738013157854448994005078112920603169 * 10 ^ 70 + 8705963627531216393441476884008499808328391376940376472136039642116379) * 10 ^ 70 + 664023131428780213925032826362663377833147257764592897482832314878428)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_232 :
Polynomial.coeff recurrence4A4Square 232 = (451337461231392083823400454395843936358491391833 * 10 ^ 70 + 2141683281152033298712764279971574078837861494422517244763529872654959) * 10 ^ 70 + 9278023093493557581988599099856781346780342958110690217636814341652101
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_233 :
Polynomial.coeff recurrence4A4Square 233 = -((184061228749705608867962422276217477581418740921 * 10 ^ 70 + 4257203592128523800744211633611130076858570692414317121780565203037616) * 10 ^ 70 + 9978278203184455940743122409012141881422890992755873086194368422168524)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_234 :
Polynomial.coeff recurrence4A4Square 234 = (73444548346850233120491989880831688816375800517 * 10 ^ 70 + 1791221534317479306169580639691453360434012707794829989545738065991717) * 10 ^ 70 + 7961429829588335880564315454527127983366942109245065744828781191468890
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_235 :
Polynomial.coeff recurrence4A4Square 235 = -((28630906563385700223159189064581799897391020033 * 10 ^ 70 + 3022848824710971145856082364218516096948204349960921741574086285396309) * 10 ^ 70 + 5274942297012813494073232648688462672997682060288939120211456633508130)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_236 :
Polynomial.coeff recurrence4A4Square 236 = (10876899490807753165004497550026090969712134504 * 10 ^ 70 + 4435951584059901798635623988135120131974877633375727756068752014430206) * 10 ^ 70 + 4662352164577120573833789204906880633943935830113479199416380059429090
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_237 :
Polynomial.coeff recurrence4A4Square 237 = -((4010153182041902387397965679786576913084632243 * 10 ^ 70 + 5081092307890882590374112469758317014320929153310555342679030287487639) * 10 ^ 70 + 4084729175166013867804327113152553506079683852455029491177792196378374)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_238 :
Polynomial.coeff recurrence4A4Square 238 = (1424619862770770602974181334294980994819813541 * 10 ^ 70 + 654426776882495169377318529067988116872939455910444645598659930864839) * 10 ^ 70 + 6370914687686280347490402249338129806097147366220324609456638973942054
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_239 :
Polynomial.coeff recurrence4A4Square 239 = -((481402160605715353824800282597551798710386104 * 10 ^ 70 + 350943089520132276304672285341340716314902706457828140911507345617207) * 10 ^ 70 + 2968094493114622899718077557218247533673066230168452958679073513114944)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_240 :
Polynomial.coeff recurrence4A4Square 240 = (150814003708600334689468173676746520219541343 * 10 ^ 70 + 4293997418577022447689132261479272595891706525285968693814754345878656) * 10 ^ 70 + 628739684226077446589249716335316945441056410992870429334406079012263
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_241 :
Polynomial.coeff recurrence4A4Square 241 = -((41219337098227641049188619063138316858461342 * 10 ^ 70 + 2873463372340363260191972436744171753174459681295383645897871652809789) * 10 ^ 70 + 9785026992650745719620565020744671211283616492118834108911686276386736)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_242 :
Polynomial.coeff recurrence4A4Square 242 = (7951633227299256341857780811570982302603058 * 10 ^ 70 + 952781203074019560090342782741653076777664759530341349796080250145951) * 10 ^ 70 + 2998502525121153070018747662403805179816678903034978525306975232170446
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_243 :
Polynomial.coeff recurrence4A4Square 243 = (553508804672517185250606757512073270506886 * 10 ^ 70 + 6151817816308393581580756094585966108799911606578864483279408469835849) * 10 ^ 70 + 9053749981807150107216707297520476488791723773541771968702874259553414
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_244 :
Polynomial.coeff recurrence4A4Square 244 = -((1821349884975631401632426465622100827982703 * 10 ^ 70 + 1038167438777899590268615308561107094962171870187763886743796799142693) * 10 ^ 70 + 5722702708078112268012737733312279084805736782768531924057337651849149)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_245 :
Polynomial.coeff recurrence4A4Square 245 = (1398688422480095937643768166122495297517583 * 10 ^ 70 + 9017369386907710775289253828641318371122615967720659516254732925160782) * 10 ^ 70 + 6040860914553697699409692539193634725445516497802456767151212785850176
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_246 :
Polynomial.coeff recurrence4A4Square 246 = -((832833975761331623783840198805311029814235 * 10 ^ 70 + 6375829542184076299768026838236881555342966344107517488564878016315949) * 10 ^ 70 + 8118662987170325191984906583289625939841728950003841232009103268020833)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_247 :
Polynomial.coeff recurrence4A4Square 247 = (441100780104237099283582472077819318383077 * 10 ^ 70 + 2988607998125540006588679792428858966171960353490791569503430207054510) * 10 ^ 70 + 2799487062478804313764611695385400150768442867521792836414897338901754
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_248 :
Polynomial.coeff recurrence4A4Square 248 = -((217392405413474742886769779826160848499171 * 10 ^ 70 + 3099986634023406094584206085519661082963845423600406597059885301605048) * 10 ^ 70 + 8239461339888052365938073027841878261142878344096508367349881380638915)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_249 :
Polynomial.coeff recurrence4A4Square 249 = (101692422626176305229235542347769455180085 * 10 ^ 70 + 3487794440308386651932750058024339843590181277050997865446545913063388) * 10 ^ 70 + 8845675170733729662355417896997005409088448097083973087942841638329692
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_250 :
Polynomial.coeff recurrence4A4Square 250 = -((45605644560845772425388147654709390905260 * 10 ^ 70 + 7129968352668274466756284497147189298931405102680819472442327970630743) * 10 ^ 70 + 8423250234102116514365160196387327661534815125520500208058457618199205)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_251 :
Polynomial.coeff recurrence4A4Square 251 = (19714480869006677001150494087463191100912 * 10 ^ 70 + 4674170101209207959603220286632181228208818471679157379121442344106936) * 10 ^ 70 + 5992073161892982077171335216863383982961641260851867430210212625697582
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4A4Square_coeff_252 :
Polynomial.coeff recurrence4A4Square 252 = -((8239185022821842923548259068891136683096 * 10 ^ 70 + 7837123382474581649436479865432571490646066701271086849087883464594223) * 10 ^ 70 + 3826746141195144365356384949438178041421629575408343337793299624941245)