Recurrence 4 lookup certificate: Scalar1Second 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.recurrence4Scalar1Second_coeff_43 : Polynomial.coeff recurrence4Scalar1Second 43 = (13363487203 * 10 ^ 70 + 8286923521390587419696826038979206867485940757149421573026899271581446) * 10 ^ 70 + 3326065058703710542354145729876101165051585645002578144991043352423510

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_44 : Polynomial.coeff recurrence4Scalar1Second 44 = -((1112547353141 * 10 ^ 70 + 6539308356060534532707328564040357918896144026985132031756301721586544) * 10 ^ 70 + 6813106742093882073397658074474184053112171269467712299358058191789041)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_45 : Polynomial.coeff recurrence4Scalar1Second 45 = (76512717934902 * 10 ^ 70 + 1838650413993188565574636135945774568975679219672204198091478585022106) * 10 ^ 70 + 3295769244953011526217595402327295823844756278080803277370262479693703

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_46 : Polynomial.coeff recurrence4Scalar1Second 46 = -((3875635362144529 * 10 ^ 70 + 7447273403637954977427962223776515093857136791499921548944471011024307) * 10 ^ 70 + 5062540786768067302394635314913154965986083125775581624854124346373105)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_47 : Polynomial.coeff recurrence4Scalar1Second 47 = (62049266652454143 * 10 ^ 70 + 6926319397984837641289432479875933750295921711504482045002203914764092) * 10 ^ 70 + 3979167664894684508211905068554027265828619096488973723100900436495657

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_48 : Polynomial.coeff recurrence4Scalar1Second 48 = (16307957003077802363 * 10 ^ 70 + 9813878617967353105764579523373974319432429340757295279248307258405481) * 10 ^ 70 + 43753681674109550089221051439906765497223755659980644012625875010055

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_49 : Polynomial.coeff recurrence4Scalar1Second 49 = -((2781678912555335689253 * 10 ^ 70 + 5725358103026850657833917153162156601723582662541795525451991807222472) * 10 ^ 70 + 2832617003479688485175107487549775310917294564840890586599784485444894)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_50 : Polynomial.coeff recurrence4Scalar1Second 50 = (302592226294341766135289 * 10 ^ 70 + 9060996372974384266394081041487213850807842019196191597383396840673291) * 10 ^ 70 + 6703688632214399798302366331895393776599705876671276826826711391927824

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_51 : Polynomial.coeff recurrence4Scalar1Second 51 = -((26900213583834822298577790 * 10 ^ 70 + 9555235546062042251114298474063133922471889797577282365085476716352405) * 10 ^ 70 + 5289980299335765694452521471591394315965564484964316133698122784395621)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_52 : Polynomial.coeff recurrence4Scalar1Second 52 = (2093687569635902176166939677 * 10 ^ 70 + 6419193918739562389898469269828997171108833577753413091211705828270568) * 10 ^ 70 + 4838954938321635985563800236629607486706128843669783139574356862101276

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_53 : Polynomial.coeff recurrence4Scalar1Second 53 = -((146989244554405261300038980760 * 10 ^ 70 + 207070494372213749270050135796431734303005107094111789636618054656710) * 10 ^ 70 + 6109275865461639969164488067757623375104891511845208756961799053624639)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_54 : Polynomial.coeff recurrence4Scalar1Second 54 = (9458895420227966807758073300719 * 10 ^ 70 + 9263849862972683365215749062576940670842177120310597055391855248726714) * 10 ^ 70 + 2687204002393044023681000199041259525017978521245808420744968741740250

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_55 : Polynomial.coeff recurrence4Scalar1Second 55 = -((563438183225537894787199603785792 * 10 ^ 70 + 427379254240743805061440472282438314194099727222872567841794966197584) * 10 ^ 70 + 5493095706124906917346377283883203331305916704617303821371721916351234)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_56 : Polynomial.coeff recurrence4Scalar1Second 56 = (31272775380886608632480226205861824 * 10 ^ 70 + 2620320624096471535747988334806095927712915449614350572345542267808425) * 10 ^ 70 + 5255959490567703554103686915933261182727070330774967738655862281367123

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_57 : Polynomial.coeff recurrence4Scalar1Second 57 = -((1624978055789363818234727645937166222 * 10 ^ 70 + 1683344178794677644654706521725245586526878262414262467898931567799825) * 10 ^ 70 + 14553808861978417738776169927590039462929239572076829008208096699765)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_58 : Polynomial.coeff recurrence4Scalar1Second 58 = (79327089037597508705764221908580233009 * 10 ^ 70 + 4987580004873314780466701334642504121221463853877105873826180591535068) * 10 ^ 70 + 9690028613686847972682208247246870812067971451829815597862099036703207

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_59 : Polynomial.coeff recurrence4Scalar1Second 59 = -((3648157418793751727024489840650537927377 * 10 ^ 70 + 8417956230845401768808208386075050309929951572807145915989794679513239) * 10 ^ 70 + 3308219633262261393120512386055846205749544307871018385411719377392502)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_60 : Polynomial.coeff recurrence4Scalar1Second 60 = (158394619845056610420448113332024201787164 * 10 ^ 70 + 7494785714016015598121164905111317210405681299702182310959592554568663) * 10 ^ 70 + 2021065231651545082679132182618564989665042970768373205372636267712825

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_61 : Polynomial.coeff recurrence4Scalar1Second 61 = -((6503852541715651886547720757817855938715732 * 10 ^ 70 + 1597735047131207132404921135814641924142115829821706757877285261939330) * 10 ^ 70 + 5902073990429682852977363691647968172882457960748011805415435223432526)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_62 : Polynomial.coeff recurrence4Scalar1Second 62 = (252907611082918772373976376216871346798540342 * 10 ^ 70 + 2419841353109400559426039762729733372431425793053669216709733964255166) * 10 ^ 70 + 5519884777483053801945159031013743958162994605454076365776081937886055

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_63 : Polynomial.coeff recurrence4Scalar1Second 63 = -((9323580641335413698883267721279278969248387840 * 10 ^ 70 + 5673741528034971171199043082132793627548030982314211433228810733010341) * 10 ^ 70 + 3800136003675502421208301358803369919833272808868278599410308012076317)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_64 : Polynomial.coeff recurrence4Scalar1Second 64 = (326125251331428782690949216515483401232796407834 * 10 ^ 70 + 4397501009625699504410239789325926798759555175590835287922845392021368) * 10 ^ 70 + 634085489698098403304369405217177160542779912072601690605075209311467

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_65 : Polynomial.coeff recurrence4Scalar1Second 65 = -((10829378162513013765623009937046754857009931270359 * 10 ^ 70 + 4649305628384741970904098224789335078891705371838477009737597613544325) * 10 ^ 70 + 2331150816390130737674044430997243968527866527247684904209916464405478)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_66 : Polynomial.coeff recurrence4Scalar1Second 66 = (341472814276140021263964998083658929320616715546332 * 10 ^ 70 + 5059020472036021551135738800602263908291051555329762305304208344390612) * 10 ^ 70 + 5650558852538764752719277229934387433911905135547285069718532988881961

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_67 : Polynomial.coeff recurrence4Scalar1Second 67 = -((10224043483105576133553906296673864792795715317164420 * 10 ^ 70 + 5237261978630290945445667527503248247297346276945135852517215920756828) * 10 ^ 70 + 1653838055714846323526941293773737484781936487557110530189205190285494)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_68 : Polynomial.coeff recurrence4Scalar1Second 68 = (290549343732831706834598006959522495080349526109019848 * 10 ^ 70 + 537469922738299803206309333039948485336209288817412089693369302659220) * 10 ^ 70 + 9469558662717818838169320319262874032300154562146498349833408546740186

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_69 : Polynomial.coeff recurrence4Scalar1Second 69 = -((7829859086896803528460370127666766048057698616306872925 * 10 ^ 70 + 478489631662833131088692186272252930371551280169888638170978943484021) * 10 ^ 70 + 9179112046918345781729497988147215651350668498683341360900952752793409)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_70 : Polynomial.coeff recurrence4Scalar1Second 70 = (199775910879583997044631827907738338972845106211511426105 * 10 ^ 70 + 8977551635397033556622964833586402472177154927118137714883452705788022) * 10 ^ 70 + 7638477497298729968526244530948090735455474155628475978457935732771546

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_71 : Polynomial.coeff recurrence4Scalar1Second 71 = -((4813790255661651732843961280076167285045531684668982675011 * 10 ^ 70 + 3694091870135586748124592660077228678357878671714640918486784525196906) * 10 ^ 70 + 580626493716009203663112412191011796020757809168312818014823183428585)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_72 : Polynomial.coeff recurrence4Scalar1Second 72 = (109102862409731779360228955463799250210765332289052397954441 * 10 ^ 70 + 2995822355832252852498944183908742884100566564840356066983565271852401) * 10 ^ 70 + 2130083134929167178083144901059722877710821892770501483341348882031507

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_73 : Polynomial.coeff recurrence4Scalar1Second 73 = -((2310747964675155680500277545763405872687304086790351748277310 * 10 ^ 70 + 2114018420643319351799348452351543903616430865771872163250436497422651) * 10 ^ 70 + 4500941210061616412353493223655118041207051559726384492815181957029658)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_74 : Polynomial.coeff recurrence4Scalar1Second 74 = (45227078972290098366094813085613045744316292421498484726910513 * 10 ^ 70 + 3640826015948029553758689275563134319753121293559794236477901046869675) * 10 ^ 70 + 2581507631099365011370463848676296591449890001891839464319374136879688

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_75 : Polynomial.coeff recurrence4Scalar1Second 75 = -((801225131469620572758144814035163487813737051572439214014602284 * 10 ^ 70 + 2710606646193013900310867376996064083347734827688502101931632486225226) * 10 ^ 70 + 2186585881999729103427118402097937490536653316483724452180912726116093)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_76 : Polynomial.coeff recurrence4Scalar1Second 76 = (12280154812546290702064157630053417355933220603854633166400381744 * 10 ^ 70 + 3610498219936193740406892060446224655851073027415013664736074162462822) * 10 ^ 70 + 9521562798396746385568468761342775938500052840501221004379896305106280

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_77 : Polynomial.coeff recurrence4Scalar1Second 77 = -((142632045093989035120483611148968250572331446722555397903852545303 * 10 ^ 70 + 2413896819763762476062429341320804346577294945492116900736296035473040) * 10 ^ 70 + 3919250631888625201443903067059857102005160839920633408708128481919312)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_78 : Polynomial.coeff recurrence4Scalar1Second 78 = (445223428423989860017286271646788039445311089369280361542759257582 * 10 ^ 70 + 4251193447493157894321391725952806885371269481899524187794542025565769) * 10 ^ 70 + 7468451273012946701651212626147600513979466961331822003304917967455444