Recurrence 5 lookup certificate: A3Square coefficient convolution

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_129 : Polynomial.coeff recurrence5A3Square 129 = -((996733870989543635284145135357710128253824767567210668626755779 * 10 ^ 70 + 4168036005507334405414860551250534900404865000480083169426957503938744) * 10 ^ 70 + 7954994228637902345029838838039612165908052300467063722906788632791046)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_130 : Polynomial.coeff recurrence5A3Square 130 = (1814627681469202915661427840121524406465666150955101285199956998 * 10 ^ 70 + 8780865859265260125088763154580759139913080174100654679465302468642071) * 10 ^ 70 + 9478933204900502162335888666444183536494232361236453720924780489956831

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_131 : Polynomial.coeff recurrence5A3Square 131 = -((3226075719531264362477656513071540383370322115023516797655934705 * 10 ^ 70 + 8656479269749818954705114097410057083660637757681611713702326052276452) * 10 ^ 70 + 3685618589377721707763886904526560501626392144627027605536347070667840)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_132 : Polynomial.coeff recurrence5A3Square 132 = (5600239250233129793263870706084489067122184398305354314276888904 * 10 ^ 70 + 9517474624928006465393630784215794343632833772956403843833965060180137) * 10 ^ 70 + 8810465527168465679354132644320858693230908908636022875991504325342149

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_133 : Polynomial.coeff recurrence5A3Square 133 = -((9491674690120239620648737422326972585437524162814925220762751698 * 10 ^ 70 + 832844371771010509783390551979229607776943365990080069750886300831899) * 10 ^ 70 + 6369301357618252506721190855628886622691490247693465837678803083328598)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_134 : Polynomial.coeff recurrence5A3Square 134 = (15704883035419650130808683478309013285722578727120188820222400908 * 10 ^ 70 + 3045052874215611973178251196899498396781591398286428225467528678248752) * 10 ^ 70 + 7118280928596554272787228279428750417736016764719072019379605550352785

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_135 : Polynomial.coeff recurrence5A3Square 135 = -((25364402188409263545894209919624985355884226088457760939397288824 * 10 ^ 70 + 5673074312690078500644222547060586173008623641065658685713879296597313) * 10 ^ 70 + 7006823113064350748753335366487275904938979420524493437002209418429844)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_136 : Polynomial.coeff recurrence5A3Square 136 = (39980200334826957355581637319054816772324516005666459038103387139 * 10 ^ 70 + 5955358192154969254141923189434989868459596547248091192289888634607941) * 10 ^ 70 + 7562730309101816758324391398052827448903012619128032714915353053211344

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_137 : Polynomial.coeff recurrence5A3Square 137 = -((61491690491918186705438927429336180847907054017892519558881322091 * 10 ^ 70 + 9481668698166660844303519300726222860258715337330087662616207686284878) * 10 ^ 70 + 5802820836414917926492827306469832904583569192572965982850142924907574)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_138 : Polynomial.coeff recurrence5A3Square 138 = (92266971410337212670405083055956880650075708075756735734828496802 * 10 ^ 70 + 7506045028448793236837858686782750983509705398666320614475390165437767) * 10 ^ 70 + 5053923461091846610117463335621713248688075924586295419300647733446450

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_139 : Polynomial.coeff recurrence5A3Square 139 = -((135028640231729459684015562453849868779891478667335061200896659300 * 10 ^ 70 + 9980539282031739265786666426930303584285563059094613016944605439573573) * 10 ^ 70 + 508831801800721419410593896630735545714432885241038044297274828936756)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_140 : Polynomial.coeff recurrence5A3Square 140 = (192676178647735967474305884341069328210014045297455234135054037070 * 10 ^ 70 + 7022149447717225417056133678926033965299720281565834316947987511825731) * 10 ^ 70 + 4835189549521200191865698887994324506933369861813323145723933596323802

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_141 : Polynomial.coeff recurrence5A3Square 141 = -((267980332579399663891702837384129251567914192710700874278432831046 * 10 ^ 70 + 2740971251271040438539719961736196043763566902480018029083314261126299) * 10 ^ 70 + 7351499929409932528843350364638863421712787937486523531562584747793494)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_142 : Polynomial.coeff recurrence5A3Square 142 = (363139610165395166381448529151691717800906125170113887787844990623 * 10 ^ 70 + 4116147733217912133600018290261648460609612192282470147002960431587042) * 10 ^ 70 + 8893818725349568432216022193788311233057875359885942774688206020944885

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_143 : Polynomial.coeff recurrence5A3Square 143 = -((479214192425595181844917955505815974752267414294575876403993542336 * 10 ^ 70 + 860330538597800727488169551530082260175827767027390619973885098669292) * 10 ^ 70 + 8495581696687002381149079154722745538001633378397289149996681166255236)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_144 : Polynomial.coeff recurrence5A3Square 144 = (615486872836267079704770142427501733037186014445125364698524257768 * 10 ^ 70 + 1565872550163480757673881522380711999868515444604265836721762124209614) * 10 ^ 70 + 6342916024594194584923106937071492246770078619164764255806907177074141

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_145 : Polynomial.coeff recurrence5A3Square 145 = -((768839412145683769807045079102633983015424452636797207233449240447 * 10 ^ 70 + 8179679100778336591319968808681910465664996298288775343724169059819299) * 10 ^ 70 + 1549747213526733981063068146196570624723420645184561973565640775590566)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_146 : Polynomial.coeff recurrence5A3Square 146 = (933267626111969692645209949164669008385701624409162590173014271049 * 10 ^ 70 + 72495117502431052629870730368450882397908488599586567328237144647453) * 10 ^ 70 + 9466715493864678523579110441025978686911317918581748611757708716866969

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_147 : Polynomial.coeff recurrence5A3Square 147 = -((1099678690833265995612966964004727628243971182274957508836703578444 * 10 ^ 70 + 968340682297204636826686107527809945266569169143083323221163770232603) * 10 ^ 70 + 4965218125142684708719133133009169990097707212033761052514508554948126)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_148 : Polynomial.coeff recurrence5A3Square 148 = (1256108258128035242621126915357590650496180969323522761893945754979 * 10 ^ 70 + 1832480589679624536660511507756749773135664073085776887396702947028904) * 10 ^ 70 + 977653307266375625310654738367489344430710342562149214142941514374495

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_149 : Polynomial.coeff recurrence5A3Square 149 = -((1388454716146650427776327758547593306828686780614612060318079346146 * 10 ^ 70 + 7142444824851216831811192003262975779236537929380842657777204292353318) * 10 ^ 70 + 2554890548364062617664603691839012673610993366095768942810433065989956)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_150 : Polynomial.coeff recurrence5A3Square 150 = (1481751683869969722640382649129139728846740292896132102083173261537 * 10 ^ 70 + 4581262906628586976434831554502980904903468407698601172195366967441768) * 10 ^ 70 + 8894101204391276340731390256633699585448025675178256394744528998403234

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_151 : Polynomial.coeff recurrence5A3Square 151 = -((1521895496481648718542346746453654776872696379523637087304874640358 * 10 ^ 70 + 711111843943532808010261975192062194843230183123973282912976031879641) * 10 ^ 70 + 4143893625781365059012167797524392264269288838496941563094065549225854)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_152 : Polynomial.coeff recurrence5A3Square 152 = (1497630156266997820878783443673123921948095938842626773461202095495 * 10 ^ 70 + 2573876404061973298795382813495694572875880041919976258730542130850028) * 10 ^ 70 + 5974748757564090418259536381954506401562711378031254855148657118288732

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_153 : Polynomial.coeff recurrence5A3Square 153 = -((1402493969127510626858012445302702633773330743365327624398094182291 * 10 ^ 70 + 9526052374607459836250574703888169276923559591331634109473604323927896) * 10 ^ 70 + 8882786786791090944593836787393776486282313531976379690830722748103576)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_154 : Polynomial.coeff recurrence5A3Square 154 = (1236378104371150462887449623214714883675711967671418948558155549007 * 10 ^ 70 + 8445881621663810154066741602146754547703994097110408622521621661958657) * 10 ^ 70 + 7457308537875954103333790448106659671394594414101492413842596636782021

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_155 : Polynomial.coeff recurrence5A3Square 155 = -((1006360376810882492079681159456241302294065825364196178706682070273 * 10 ^ 70 + 3507947351137837074774223641333147689292616328104777675578209802352273) * 10 ^ 70 + 2084264132182283877503479301593251268135872094683612463332789568893496)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_156 : Polynomial.coeff recurrence5A3Square 156 = (726567135405850897862001792114410713323513006759163707244894790424 * 10 ^ 70 + 7576189545026045025526591099339360364175893057765849331801157064515448) * 10 ^ 70 + 7840801199018409642647822852628606174679670913269674635277368412135946

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_157 : Polynomial.coeff recurrence5A3Square 157 = -((416973139222589725788707450398728371172366660252444911065154903519 * 10 ^ 70 + 5625104272904119498941819092633875969700328111671041793750616789314120) * 10 ^ 70 + 7167959876717399319351218525272249739996000795690350075460576886428994)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_158 : Polynomial.coeff recurrence5A3Square 158 = (101245473449333062911498652699106612526293358935604980916205629989 * 10 ^ 70 + 3287519468162456245283445347860882923706884988240410069946869490704132) * 10 ^ 70 + 6751883580677840908336389864495247370193984419651699394249960190882137

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_159 : Polynomial.coeff recurrence5A3Square 159 = (196069220101287954880260078334796014939293381096260162068168634804 * 10 ^ 70 + 9241629809551428552624955555562470025187659445251793485863067759105993) * 10 ^ 70 + 2333145180644191182748863922176444078245437808879234890922897358552420

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_160 : Polynomial.coeff recurrence5A3Square 160 = -((452570519694790753668104508363162201456516786621410943687033686377 * 10 ^ 70 + 7506657887810563633801804200943749806372273937449988384756480107686868) * 10 ^ 70 + 840265504689033680564703143435437514960559926769406183572555519683202)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_161 : Polynomial.coeff recurrence5A3Square 161 = (650740952662830912429751191836100930711649382743870237161179842500 * 10 ^ 70 + 8752716870257719460396898863785468637112351117127116477807949812657629) * 10 ^ 70 + 1624818784112829320146917642156349887838668030664075756008746266042312

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_162 : Polynomial.coeff recurrence5A3Square 162 = -((779936907661086548885091540691512986782323508738621994484604633814 * 10 ^ 70 + 8830190405250418636386140484862363278526593625508077297046100600744330) * 10 ^ 70 + 1091219794624112385457483621197766624176460387819729571780615787176455)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_163 : Polynomial.coeff recurrence5A3Square 163 = (837318115446979635495087694903284866101427140478437938463293417537 * 10 ^ 70 + 2712858652617545113402551206760491108443038654489997639747755827677143) * 10 ^ 70 + 6167806090240560858299282513939504919804964531592790073412518566328190

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_164 : Polynomial.coeff recurrence5A3Square 164 = -((827605214713464825219866873697743967097915724868492662002340922419 * 10 ^ 70 + 6592097480285415548893601645100117393217943132237794333578769586145835) * 10 ^ 70 + 5827346839643299711989434168934988016398276380936740703796002986198819)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_165 : Polynomial.coeff recurrence5A3Square 165 = (761776395750897860001676882701927981774909967221639014797457011014 * 10 ^ 70 + 8197688070159743007640686975850722281612998495843481784853268571405582) * 10 ^ 70 + 9200629076069655035045712423752922299161705140176971950981110779325986

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_166 : Polynomial.coeff recurrence5A3Square 166 = -((655001459518548318380337527108124069506388780212302546174053126637 * 10 ^ 70 + 2033493412034869329046767160396898170359839458220235669237265778928487) * 10 ^ 70 + 990724237116850289130006510846164371667270343223991895445106089932607)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_167 : Polynomial.coeff recurrence5A3Square 167 = (524224977263957768957460841823558454489630417630360968767528156878 * 10 ^ 70 + 57459879090861845110785187139172651213693435546200677823586905261657) * 10 ^ 70 + 4197850333885647022929090825816669106875160900162014331207827640548218

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_168 : Polynomial.coeff recurrence5A3Square 168 = -((385830243214283869097874490813317374360436565447461371267921207637 * 10 ^ 70 + 4267158747196068785727681183062183804999481806058965226505129669262741) * 10 ^ 70 + 1992063223744970347339282156152238003521965313560949459664835940583435)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_169 : Polynomial.coeff recurrence5A3Square 169 = (253747114393593449536030776044437150893574118724292180234876556467 * 10 ^ 70 + 7752527768760132640662682663809575446250760174502647867634132191315506) * 10 ^ 70 + 627275818872975751136043523459920058646363903898996587371001343372760

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5A3Square_coeff_170 : Polynomial.coeff recurrence5A3Square 170 = -((138235003035896504637634421387034539552754981749327691077872196979 * 10 ^ 70 + 3162843225189385776035310908316682188518301961431271675181262020307734) * 10 ^ 70 + 8452741673921032958238765868759081660195691776636215770608770979099137)