Recurrence 4 lookup certificate: Scalar2First 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.recurrence4Scalar2First_coeff_135 : Polynomial.coeff recurrence4Scalar2First 135 = -(((180011544192083890856624659995347251574532967512848386265 * 10 ^ 70 + 3431824470914981603605145987148838377644871815097350586675220048781099) * 10 ^ 70 + 7043327682544307377854478258931887718082673080832233784121077701426938) * 10 ^ 70 + 4927014149520823771181033860629934288689280844482664366058576040874083)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_136 : Polynomial.coeff recurrence4Scalar2First 136 = ((1002228748330007235886381119128549344503174451882293596986 * 10 ^ 70 + 1781157804698553471892814544257276487289092422749573536965906358421583) * 10 ^ 70 + 5138657786674785282854536506702685459910898840526950421368788617607739) * 10 ^ 70 + 6690404415925987496546977619265437708853606906742804623694546449620730

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_137 : Polynomial.coeff recurrence4Scalar2First 137 = -(((5476852908987378148662580912658001297812529235053988949859 * 10 ^ 70 + 7939355404293759555348538896981105136740804733147039565238874682278611) * 10 ^ 70 + 4161489851166606561920114908446662963543910364103351157258755437516854) * 10 ^ 70 + 1278759846489516820094451008092647186952272438841964405901141191845018)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_138 : Polynomial.coeff recurrence4Scalar2First 138 = ((29380565805858881903260830581584462513145094313736850295126 * 10 ^ 70 + 3758508761050444788056910741089775443341099927735775806965841492434755) * 10 ^ 70 + 4216962494851861820083761514705062804046647104127002840943295531398730) * 10 ^ 70 + 5894243587083591608972071167241172309949260072101477829334086538886843

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_139 : Polynomial.coeff recurrence4Scalar2First 139 = -(((154745960008811971184850981776125429688811549819227934318774 * 10 ^ 70 + 2431944973469564452463242385877330879572895706120345897083325795326655) * 10 ^ 70 + 8374051304667599235357971092579035431440570532111743253171363068297521) * 10 ^ 70 + 7131323694536410990461072329292061387678182873292802152997317776610780)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_140 : Polynomial.coeff recurrence4Scalar2First 140 = ((800335291703524337270644256600183919153212001938722028571333 * 10 ^ 70 + 2280690219675111077699487342490365441531340784200688565829759749628838) * 10 ^ 70 + 9831502117930350759202597326261760862859893358942635772787034307937230) * 10 ^ 70 + 7496364424641887611823538844948322538361078108471835787919725169512302

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_141 : Polynomial.coeff recurrence4Scalar2First 141 = -(((4065179535766720550622721822734078195225240907255434289450499 * 10 ^ 70 + 7327846069929714903218342772292597700338877861420857803357328909034321) * 10 ^ 70 + 1487621640497160444388942289799058648089890397262254686790855607952064) * 10 ^ 70 + 6267366125680878178826173002371838967416544286545885253427187055721043)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_142 : Polynomial.coeff recurrence4Scalar2First 142 = ((20281614912343762060350662769181219574269230401286300485844365 * 10 ^ 70 + 3131251865406317611461254295500473526178068294768297575531107252747278) * 10 ^ 70 + 4194620810398510934704859819737419871397489254364211618954639420327826) * 10 ^ 70 + 2187049389445259364908868690390263684749461873531989316388413729677877

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_143 : Polynomial.coeff recurrence4Scalar2First 143 = -(((99402807570212626575370619430044987669369779475402788395860961 * 10 ^ 70 + 5157594635120212788860820102475707499292450140014704954209763069364763) * 10 ^ 70 + 7093198577729290726512307029498686640881704348473228432232736513493823) * 10 ^ 70 + 1382555421339408985603251978259982856536696753857218895944094566230769)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_144 : Polynomial.coeff recurrence4Scalar2First 144 = ((478657391794455437085720954120945205981823008579079881210100442 * 10 ^ 70 + 8899970425427723852816494345126866562136323068118027212701457132160645) * 10 ^ 70 + 3658897014837890724545418294381636624255309807606031976961302539058777) * 10 ^ 70 + 3088641613339754698579358394622600240431151926744611649756134197752305

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_145 : Polynomial.coeff recurrence4Scalar2First 145 = -(((2264832201462555152110211081582827500386084369857531286895159091 * 10 ^ 70 + 5376379660254241699443120352858581514888085239714653912042008820068707) * 10 ^ 70 + 2339354875771638049990170041607287415292086374731616357932850819625324) * 10 ^ 70 + 8214622349203494638263284021720308511425710920111703744829600722104882)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_146 : Polynomial.coeff recurrence4Scalar2First 146 = ((10531399354504203319202116218534021209728659131486883391275625056 * 10 ^ 70 + 5876131367179353019718819201243092270755922927950029671584923521963761) * 10 ^ 70 + 9678238719255338040708691441217667565110629828949118867535129538300657) * 10 ^ 70 + 2151742358009415772239488223456163198157646896985225380797564862819266

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_147 : Polynomial.coeff recurrence4Scalar2First 147 = -(((48131247651155045773012313399937320940597665023323872368310639032 * 10 ^ 70 + 8740493475061944518688304183575967728897320041971670292442702717504147) * 10 ^ 70 + 8472460711378288049392899154291090601000113641519728965415877969326737) * 10 ^ 70 + 9521820095400098371513243643307303179404085659977363293320317535531796)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_148 : Polynomial.coeff recurrence4Scalar2First 148 = ((216227007012734650162536268463803302100986157852094626882741255464 * 10 ^ 70 + 2792898957056807273675000693536971197428932609329228876539831817026231) * 10 ^ 70 + 4016529445866094619260105047258370425936663340001335974332963179124245) * 10 ^ 70 + 7486409533233085220591710791057702311682980139532183897422348397190694

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_149 : Polynomial.coeff recurrence4Scalar2First 149 = -(((954957317060552086028017964034540157093661255466558147487954716657 * 10 ^ 70 + 1398134139029240096683460323066625779036047892413164582975907339662702) * 10 ^ 70 + 3585696964987479529201253927185516064258333820241187742691252320899433) * 10 ^ 70 + 9017183429102095270289543895855349420442808819535133818583939733867350)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_150 : Polynomial.coeff recurrence4Scalar2First 150 = ((4146649154259387421540851083906629545611884523484038086141355165734 * 10 ^ 70 + 5502093027156925249005805560584512925291717845117647462889867369826255) * 10 ^ 70 + 10051135889964862405471587663314398160632807988225743644627617116320) * 10 ^ 70 + 48980499450348128970988669131063874652723461070710152274500087867423

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_151 : Polynomial.coeff recurrence4Scalar2First 151 = -(((17705032990267336746824923810006323018691640958673383023330754456779 * 10 ^ 70 + 6540005836472031547928415829022918156974559221822795502767226243548794) * 10 ^ 70 + 7501829310729069594860231553713429365854786863153747494608791322665201) * 10 ^ 70 + 7363587085608982450652563870243516182691078365286143305470108798528552)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_152 : Polynomial.coeff recurrence4Scalar2First 152 = ((74340908478625699504379446910320593358486053230790520712313931612675 * 10 ^ 70 + 4964151685751705274697732189142259362181429670897074096722155988577668) * 10 ^ 70 + 6935955345676248558283244137574935314444414555736768906273852284070017) * 10 ^ 70 + 7895571007031016052848632634818676996527834667876824120163130322455818

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_153 : Polynomial.coeff recurrence4Scalar2First 153 = -(((306997613202565783579107356091263989512946323302195733320993186550060 * 10 ^ 70 + 3043979126663146248063890552791211743159987375444269606931713137092989) * 10 ^ 70 + 1057079896296276500342052424615828991358658123509296144156961808365346) * 10 ^ 70 + 2904488261338181274359345337125477872383871311809088131893263423046295)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_154 : Polynomial.coeff recurrence4Scalar2First 154 = ((1246985183026721541918874282389713707488161750632476708647849746626016 * 10 ^ 70 + 2474332267131400380479647472066484815371415074504368538233515002367940) * 10 ^ 70 + 2506207412737678141480689167036865057837862416065696680770570151103420) * 10 ^ 70 + 6245156650281203292933971246751982305313740702628704814739253607662152

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_155 : Polynomial.coeff recurrence4Scalar2First 155 = -(((4982516400249822411939906348293609830007470129577830800984867865666726 * 10 ^ 70 + 2270600711004488145708153135770840130391685179382025922417763701000451) * 10 ^ 70 + 4075319454100652063733472960672368108407675086560380556755755155928949) * 10 ^ 70 + 8739409887924417722227487497396036780637745347136999229174849727661452)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_156 : Polynomial.coeff recurrence4Scalar2First 156 = (((1 * 10 ^ 70 + 9585659180697986698464935028558997928739341676122464195302062405073455) * 10 ^ 70 + 523497892762364070885386378261778909039344653527657097301816136135623) * 10 ^ 70 + 6735735600212725120376084551588755861257768369686868805399982521201113) * 10 ^ 70 + 7443610060549382379743633051479398100646910284050243566341263165013876

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_157 : Polynomial.coeff recurrence4Scalar2First 157 = -((((7 * 10 ^ 70 + 5747695416222010917966834515496075331629943329153327153326858121924403) * 10 ^ 70 + 6283090730679536312379328202901599996850755465261831007115778762130798) * 10 ^ 70 + 554138124942248620335226279639830337763515302957066233647038839360587) * 10 ^ 70 + 121593401775430145780980751948866191301649529172194364808365006772433)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_158 : Polynomial.coeff recurrence4Scalar2First 158 = (((28 * 10 ^ 70 + 8257835855162873403576699626767489829624793963711278790965780171901728) * 10 ^ 70 + 5018519543838774035846867642058257695782449141533850480154092156558147) * 10 ^ 70 + 6035785975590620901844905669431696543075454449684075993765829481229897) * 10 ^ 70 + 3270728186209123104102328194236184221643251416281859691822952653174870

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_159 : Polynomial.coeff recurrence4Scalar2First 159 = -((((107 * 10 ^ 70 + 9470878451638148365580250861970468726797501756935642310966856470770803) * 10 ^ 70 + 7831681582040418343821307993392325039336970259753688083983167997660414) * 10 ^ 70 + 9779861915009868955236071478776233399841051206037411278361428654949440) * 10 ^ 70 + 9096144851345720223609109322906099307537721850777042524548559912693787)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_160 : Polynomial.coeff recurrence4Scalar2First 160 = (((397 * 10 ^ 70 + 8281177927295801055425563689587959255899986307745727414817065448050015) * 10 ^ 70 + 8727716434429854002097946793145395948000618948128249986041773655126431) * 10 ^ 70 + 2207851772261117537202097936076093589001686744809964481776219768565719) * 10 ^ 70 + 2180461267504590215906939299447282914862987805056044101701448909623697

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_161 : Polynomial.coeff recurrence4Scalar2First 161 = -((((1443 * 10 ^ 70 + 134635539137491055454102465884851170297373044794049113797826035473777) * 10 ^ 70 + 6927580810577956344353352118647621464280389749324350469270952788203294) * 10 ^ 70 + 5246840971751434673309266305553826626136589593163008498704335489527596) * 10 ^ 70 + 6819272259287132624998937811203701933427047437464179796398103903041379)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_162 : Polynomial.coeff recurrence4Scalar2First 162 = (((5151 * 10 ^ 70 + 9342294604044035799888419592860247511097459238547312945477989385139162) * 10 ^ 70 + 4468338754837650206289201360497120537374474713196134463807315916510091) * 10 ^ 70 + 1703695953116785098813640542552052327172651153238204230788911476310885) * 10 ^ 70 + 6401423590827722961021030516735052490106445301439039127890839817203175

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_163 : Polynomial.coeff recurrence4Scalar2First 163 = -((((18106 * 10 ^ 70 + 2686886842230521461831948386470578567664848550544334794227217375898904) * 10 ^ 70 + 1406451358882189096465888782922149288021497251681951936270252425479450) * 10 ^ 70 + 5373650121956286272356066185693957083578814462174190751338169909582069) * 10 ^ 70 + 3541763064638239414809431548281436187795697050559109576048659054736787)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_164 : Polynomial.coeff recurrence4Scalar2First 164 = (((62643 * 10 ^ 70 + 9467455537495201072063165255954398158567685653183290970551881404006870) * 10 ^ 70 + 6164839325880133862341663298609116887065191345214923695202956209232681) * 10 ^ 70 + 5463297981523869130273974193212195262049197323464450256204455046866152) * 10 ^ 70 + 652884387774462420588598997316858449396607839838924935543722270688972

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_165 : Polynomial.coeff recurrence4Scalar2First 165 = -((((213379 * 10 ^ 70 + 4697875622817213079455875836230566249721150350743170899100329599887857) * 10 ^ 70 + 7310624135640886640309724728746327818522341910504023265604606568926847) * 10 ^ 70 + 1505391191393127901225088219018624594477197654411537716308742917082443) * 10 ^ 70 + 2936935225096956329312020634358518059043865786524176603739869274161424)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_166 : Polynomial.coeff recurrence4Scalar2First 166 = (((715616 * 10 ^ 70 + 7582755540689082420339242413167911986388647916066631015681170011488384) * 10 ^ 70 + 7093685895563513124852776393605820143476414774046407727158523644683717) * 10 ^ 70 + 7910265068350385539490469267321960041656401320363880385776216377365111) * 10 ^ 70 + 9434294108600596354587485854895290410864781287914590517854732154537071

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_167 : Polynomial.coeff recurrence4Scalar2First 167 = -((((2363158 * 10 ^ 70 + 4249501193626123291519358709433106406500376571254393187408125771584521) * 10 ^ 70 + 4810010811358234059667237889773069594003803033082554268357289887777540) * 10 ^ 70 + 9288562587272146936936696053343649778692647401729833741506408832278386) * 10 ^ 70 + 7848419964419122202011115467393190370401686842779443603307212329549969)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_168 : Polynomial.coeff recurrence4Scalar2First 168 = (((7684558 * 10 ^ 70 + 1630199865498522550864673098485247738269740851331145061608613588273539) * 10 ^ 70 + 8288118749805618646200742805067366396213061327133199797378565394012005) * 10 ^ 70 + 8266418162092923103188118197618002594189902432084453038207607815236155) * 10 ^ 70 + 4978396115661421550766011551373894830242439733246703779550649762031361

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_169 : Polynomial.coeff recurrence4Scalar2First 169 = -((((24608612 * 10 ^ 70 + 6204056318763424557022648447242611406723534389239986259718609275482932) * 10 ^ 70 + 1840784688829562103040948823214801868481626042365998454174620223242809) * 10 ^ 70 + 1152791120066236253907704220132541730363245204038815075705673460850169) * 10 ^ 70 + 1394045440374798236856129144884762899454933607076956386513451376981874)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2First_coeff_170 : Polynomial.coeff recurrence4Scalar2First 170 = (((77611332 * 10 ^ 70 + 7339032365695888581503346677456928228628410468568237115580230810823091) * 10 ^ 70 + 5777429130272270265249930096095915303559510754809512149759817326425607) * 10 ^ 70 + 1791194431820914256571696602618269946096659304847276836644591226487453) * 10 ^ 70 + 1123427408891979116992579862953658020484911394586749364391750786975136