Recurrence 4 lookup certificate: Scalar1Left 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.recurrence4Scalar1Left_coeff_163 : Polynomial.coeff recurrence4Scalar1Left 163 = -((((34792 * 10 ^ 70 + 9374637661141666657893251537187491759620261143471878023977585281630831) * 10 ^ 70 + 6611522345150383806153571091957619453778076229245032449296873515336874) * 10 ^ 70 + 7811852922253660510938021278402393076750572476838208292774820890283406) * 10 ^ 70 + 9796182197503647780494569154765955785446564633008015609624710193077343)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_164 : Polynomial.coeff recurrence4Scalar1Left 164 = (((122022 * 10 ^ 70 + 57302299402328999425768403714528994271333252223598460970510198952421) * 10 ^ 70 + 5164986774225865715985217555949617635553318853018452794962391502501689) * 10 ^ 70 + 3946901000150704986250900265469852631222127991571989414462588652677949) * 10 ^ 70 + 23425089603238065483873977393186908089258421495613874111593611244401

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_165 : Polynomial.coeff recurrence4Scalar1Left 165 = -((((421295 * 10 ^ 70 + 6580294467757218965977445727020562667976832646764899406140588648713989) * 10 ^ 70 + 8796122145778512702796984094309047299426099206773756077505219025233792) * 10 ^ 70 + 4965040952830119207443279494773123606076069641798778996983052909428051) * 10 ^ 70 + 479962541810780285995835462132004926825033446165810591254449337030985)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_166 : Polynomial.coeff recurrence4Scalar1Left 166 = (((1432084 * 10 ^ 70 + 2848961183227165494390089232790935964164070850738755395215770244849999) * 10 ^ 70 + 9467272969842869151112632602605712661707741252800541301862270141615130) * 10 ^ 70 + 5010660307323983152502822923980858990217553006532285443333920347046917) * 10 ^ 70 + 6722235288440612138805326060781757549407895407536901587684765081010885

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_167 : Polynomial.coeff recurrence4Scalar1Left 167 = -((((4793062 * 10 ^ 70 + 525019286889576643510846856579521254523581411640721208646365374500960) * 10 ^ 70 + 8546914626088142560258096897766959785731349063195882799461065531647716) * 10 ^ 70 + 7933258074292532477520268168908119424848987550031587355883089169849238) * 10 ^ 70 + 7577565640047218489673379197017954849714507293800326250200911318740748)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_168 : Polynomial.coeff recurrence4Scalar1Left 168 = (((15796090 * 10 ^ 70 + 6972164559636109825034373834821879360837487213714694816875718297176659) * 10 ^ 70 + 3851231166469373593885540503323883299999522220335152136595211772175795) * 10 ^ 70 + 191126841124333266337384330422269165851229318570428228217635477549097) * 10 ^ 70 + 9233419386257769832145766031870781053389060239784916343311916677108976

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_169 : Polynomial.coeff recurrence4Scalar1Left 169 = -((((51263308 * 10 ^ 70 + 2762583625882188615462837061206869898930428247577060024095159302128042) * 10 ^ 70 + 9557358267240314878943933910137180360360027092993529053011339647169776) * 10 ^ 70 + 5851979662210708804956453029183349881764279073831782120118868906711483) * 10 ^ 70 + 3542288411421685683666067687231705470752569089976805519750781945215651)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_170 : Polynomial.coeff recurrence4Scalar1Left 170 = (((163836848 * 10 ^ 70 + 870470632800070525917342180422946122028615351346276147976962253605533) * 10 ^ 70 + 6900021178550525695730563067620150037492885864010370546369630764332930) * 10 ^ 70 + 7665296820337529311691974110237428337833754039820082296304172715122063) * 10 ^ 70 + 4554447070679459302042852463624524008133585937050800973977908689911369

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_171 : Polynomial.coeff recurrence4Scalar1Left 171 = -((((515692894 * 10 ^ 70 + 7395321055497637504294457556335620795502786987561949086413585964319627) * 10 ^ 70 + 9450710767121188498211399235894369853595763440776932319234262252339132) * 10 ^ 70 + 8654847712638051235609574545652498883926167697868075010487477119600469) * 10 ^ 70 + 6971299537386108780733684967548246616899395728127917707513489448243762)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_172 : Polynomial.coeff recurrence4Scalar1Left 172 = (((1598715437 * 10 ^ 70 + 8431004007587056549076088858559143711250919414509945268319961795261143) * 10 ^ 70 + 6835570117712310802022479627278757052344161688675201302795894504072808) * 10 ^ 70 + 8946112238246439444999082996933445595469211487584413636291886249945957) * 10 ^ 70 + 245763076130643811153606738911925740347302729173229809917408284480429

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_173 : Polynomial.coeff recurrence4Scalar1Left 173 = -((((4881763037 * 10 ^ 70 + 8341670977898171966987053004198412738210338936802368371401588543319895) * 10 ^ 70 + 1219938796130574163941192205019085813195927500822236707403209710348235) * 10 ^ 70 + 5159658205308986687882111063199274122583069238765599541907654900011489) * 10 ^ 70 + 5684830632173984491288876512219147296875874021951470513859598849795512)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_174 : Polynomial.coeff recurrence4Scalar1Left 174 = (((14683581127 * 10 ^ 70 + 3353598851369147458126815668580582308975013259355364206821075149938760) * 10 ^ 70 + 9854869203809760512568918955140813784813933975172174897351690898279888) * 10 ^ 70 + 9054593318398603211467924100881388309663728913037090978466474150187726) * 10 ^ 70 + 3306661409212967636035717419442532188546493490497231205394566623192803

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_175 : Polynomial.coeff recurrence4Scalar1Left 175 = -((((43507139893 * 10 ^ 70 + 5513166541890910005146809157883752227486005738842559800224009985986412) * 10 ^ 70 + 996029751240510955924699565814523516909660779508997182183777108116523) * 10 ^ 70 + 597243455607399783000915831218723813118768276672186372261953570151195) * 10 ^ 70 + 4576787014975818912254978299319860310682390993725118256657813755431776)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_176 : Polynomial.coeff recurrence4Scalar1Left 176 = (((126994544981 * 10 ^ 70 + 6374119168941853724994522113447271134619932647183812066197597956948550) * 10 ^ 70 + 7339811438722381724679590482631897991492108007230762184161875617947307) * 10 ^ 70 + 3825334321106267119232898375871592719212168130742776024492444825568031) * 10 ^ 70 + 2631496193856339168585177393868733658660877534522805519000689224578685

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_177 : Polynomial.coeff recurrence4Scalar1Left 177 = -((((365197307807 * 10 ^ 70 + 434877041053632362981276659867199533305104430075479193371071318913317) * 10 ^ 70 + 9912700663225962621769382425010979186319810582855633916002797293013944) * 10 ^ 70 + 6754465577370470086006321002407046227930488680959383047186729618422262) * 10 ^ 70 + 2994094802766404461338837470086167352198745357020579932182859639762248)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_178 : Polynomial.coeff recurrence4Scalar1Left 178 = (((1034687701277 * 10 ^ 70 + 4883325709053272561050458100617612719714818983830382679202077682235212) * 10 ^ 70 + 6319838256345073386921128885471106678835432836835093118186463402016578) * 10 ^ 70 + 6412198267657559173281009112034502594420558175268774599276016501662135) * 10 ^ 70 + 9865794053500412102657332728745970886584253898577507387011415146443830

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_179 : Polynomial.coeff recurrence4Scalar1Left 179 = -((((2888356209989 * 10 ^ 70 + 8686736624324390578057403371424162130033352625442954685075167603933227) * 10 ^ 70 + 6323700216796903783159778131073606922477472790660318700956242844411984) * 10 ^ 70 + 3278432297585045361149036991284466335891218626357363615030511315804728) * 10 ^ 70 + 2773545993542752740283922041575007565296749699657464875004807531873197)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_180 : Polynomial.coeff recurrence4Scalar1Left 180 = (((7944595268431 * 10 ^ 70 + 9884787082481753525149403806492616669277917058042929675794701895526955) * 10 ^ 70 + 4370920810048518282919310688280263018856395141613041468051897021762057) * 10 ^ 70 + 468549087191305670330766477057465130044764188143678444104148475891341) * 10 ^ 70 + 441753665502285367369018416627448850512271494022137185289453198263165

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_181 : Polynomial.coeff recurrence4Scalar1Left 181 = -((((21532352170079 * 10 ^ 70 + 5868209184959695635257279412085109895472879749200444242564245279568291) * 10 ^ 70 + 9889956495326566589645367713061754829394764296475484010937309479374587) * 10 ^ 70 + 4919854367955273573372636279313267403641197175125915129871308477454207) * 10 ^ 70 + 8425208349134372930490958899898148803206282109804109374664010434597438)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_182 : Polynomial.coeff recurrence4Scalar1Left 182 = (((57507999576507 * 10 ^ 70 + 7464998473934392538026536422821734709708842437867201664976103827469023) * 10 ^ 70 + 3189423403590782436530863778310335397699863728391914110974268836761403) * 10 ^ 70 + 9413749539797680697446943244283857640654852225402545836446512636456019) * 10 ^ 70 + 2489120018553138814735062613727108101941384159945834276058440507295369

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_183 : Polynomial.coeff recurrence4Scalar1Left 183 = -((((151356079285170 * 10 ^ 70 + 329924244464087443735656692860384572863371723430490854750434733472496) * 10 ^ 70 + 4061923209683879578830864892562843570495071999107224958907516128360285) * 10 ^ 70 + 6584667305635356958516914610942513010241906523322295262074360557681119) * 10 ^ 70 + 6377957175326652270351190149651518489256805144957739561909488891667107)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_184 : Polynomial.coeff recurrence4Scalar1Left 184 = (((392575645258974 * 10 ^ 70 + 7690347444891429102833923162034798599148574930090418231712924953305822) * 10 ^ 70 + 1983108151767553543923899367415601652405998026069286643405314444973967) * 10 ^ 70 + 3334903072378111425901602866961521403994648937732705006371110440098739) * 10 ^ 70 + 3242677900704637784739010799162136394735797376968520382346251982971132

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_185 : Polynomial.coeff recurrence4Scalar1Left 185 = -((((1003494725974045 * 10 ^ 70 + 2108571508639970633133831711328061675779086343730569398551414854943791) * 10 ^ 70 + 3766391814797973428252045258346691736805183998976083661977473926967761) * 10 ^ 70 + 2288944419568589722836280173200528269229932147537662003664323316855345) * 10 ^ 70 + 2032993111057676563828711331622955783534634125128332275371494037941042)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_186 : Polynomial.coeff recurrence4Scalar1Left 186 = (((2528079971442100 * 10 ^ 70 + 4483240304845749345545214626132497532794362867861617652679678373205083) * 10 ^ 70 + 4084636783939725487155428569367685771121610875731735826654041953942256) * 10 ^ 70 + 38260165075662410948519308809262384257726476580787678512250581606097) * 10 ^ 70 + 5324112133593848564742046165495115364615987088351625496702603422460816

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_187 : Polynomial.coeff recurrence4Scalar1Left 187 = -((((6277193953641014 * 10 ^ 70 + 362509822339505201334497626565835518280918479282134743349339600164232) * 10 ^ 70 + 73710539345187997980242076055834674363094096275888446497779819401039) * 10 ^ 70 + 9421824336739716473105653395486990646984238188316182755600794058014988) * 10 ^ 70 + 1360859257133219395085262746622257385269185074246220812026780262756417)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_188 : Polynomial.coeff recurrence4Scalar1Left 188 = (((15362210413687424 * 10 ^ 70 + 5515548815323999233059967268240801304812166653241479661527609138679621) * 10 ^ 70 + 4969135573303367573581185371577025936299570452372273168134148848279397) * 10 ^ 70 + 6595034127060108786065730241607158107671292041315455182530505039392853) * 10 ^ 70 + 4360143575872870344518693435033498511243653271922320661030607866831530

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_189 : Polynomial.coeff recurrence4Scalar1Left 189 = -((((37056895523871852 * 10 ^ 70 + 298950300590912001100224181487398592972266197681274248401058311323123) * 10 ^ 70 + 1353751103654122144531957167163825515342946739562512383826595953672725) * 10 ^ 70 + 6151964343611309347359218270957233492686180812634809619060828501469687) * 10 ^ 70 + 8310004554198639629258993180537602836250382306771538397705629731983333)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_190 : Polynomial.coeff recurrence4Scalar1Left 190 = (((88109879314514851 * 10 ^ 70 + 9843554819586738825317762233630387339515918902228194764345629890296879) * 10 ^ 70 + 301951102078296286770280112209485443211328020103052101879026542288171) * 10 ^ 70 + 4166233730356393979940506041887002874041537019913006396458719683926388) * 10 ^ 70 + 6475533827045767950328190196980098155576996659647657570577011690741018

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_191 : Polynomial.coeff recurrence4Scalar1Left 191 = -((((206506090037817514 * 10 ^ 70 + 4058446738071562075654812090597901386737061856024767936549223899557980) * 10 ^ 70 + 114052035198444547446194196729280603914808623926543291187212503659387) * 10 ^ 70 + 745655178506406643491808209967511557209060823114732754584224193647432) * 10 ^ 70 + 5939812966394803025651469838609908229812990375011960298879223400789924)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_192 : Polynomial.coeff recurrence4Scalar1Left 192 = (((477095793540426003 * 10 ^ 70 + 2465654270478701025095312240073055182745588959996221552363898954684659) * 10 ^ 70 + 3959747041458917973836793970579784684663325083482234002288631234654006) * 10 ^ 70 + 5906013292337706679558635379562021217547614321297686148284642912796779) * 10 ^ 70 + 2910434363426154964186217501373806709595527220721128516850517351704347

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_193 : Polynomial.coeff recurrence4Scalar1Left 193 = -((((1086560479553661432 * 10 ^ 70 + 3433785298765415578611787441276677897199721144084091727689097911079343) * 10 ^ 70 + 7520479719229386218810324691920724464862579392133458654599089227968403) * 10 ^ 70 + 528755489303432468779986656983720071668365150372684428021686784711718) * 10 ^ 70 + 7278710863858952962458966992949409831706153312720796387881890888618653)