Recurrence 4 lookup certificate: Scalar1Exceptional 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.recurrence4Scalar1Exceptional_coeff_383 : Polynomial.coeff recurrence4Scalar1Exceptional 383 = -(((18052272435675936204309057999031231258897316922678019159648781520 * 10 ^ 70 + 2209915408470326076269551367618167881741520952074775774439704372187666) * 10 ^ 70 + 5874407883950220709808609088715669753684696440527106508481559207747014) * 10 ^ 70 + 9624530974765399855583789362449401428064777619677505739387077760605567)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_384 : Polynomial.coeff recurrence4Scalar1Exceptional 384 = ((4224866243334306523135427007298476760720900432518714795590796330 * 10 ^ 70 + 1182054810369761201013308128214226390146808427618224526752042009576820) * 10 ^ 70 + 3916396197218658337275046738871373904459097778449468168724117601713051) * 10 ^ 70 + 313237541368117701399155724025943211661636755351003314623055508996714

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_385 : Polynomial.coeff recurrence4Scalar1Exceptional 385 = -(((662874295420186577683928642718118272731828662733491075917491188 * 10 ^ 70 + 59757006765952423455901313578635299021925109726067921620503995460011) * 10 ^ 70 + 4363787080733505701327012469526814313266419916479346755246000009134595) * 10 ^ 70 + 4176416954496709466018839941210842336051775608766995218236228419776585)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_386 : Polynomial.coeff recurrence4Scalar1Exceptional 386 = -(((61800650155862182105719311869660822433559686682257881943886246 * 10 ^ 70 + 5773465711003494838579454846656074907763056979153823107879985958693492) * 10 ^ 70 + 1019068710136845146917056894230754799485913567610556261869521348452130) * 10 ^ 70 + 1005746647971025068140056024289807978489570965785416515715403775155583)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_387 : Polynomial.coeff recurrence4Scalar1Exceptional 387 = ((120818288829698441399129998540397926581259992583710305011496277 * 10 ^ 70 + 1985003664291952527771503494571728021469608110677688020460673335507843) * 10 ^ 70 + 4596073970856662097010505986519714610884063599631522526456025438956533) * 10 ^ 70 + 4279630833821688505055584155397416679079647113868270011482341442214321

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_388 : Polynomial.coeff recurrence4Scalar1Exceptional 388 = -(((74249969692121822178946750915769117687780874808778624101679941 * 10 ^ 70 + 8110395430909268630103340707653801933482262792801782123535639632069146) * 10 ^ 70 + 425195509608745278272838838725899460282846041734687275240895334852811) * 10 ^ 70 + 4461446659647160538124036834401965823152108236120986844190257897004344)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_389 : Polynomial.coeff recurrence4Scalar1Exceptional 389 = ((36120050517835347782257454690889594211901757846307060384601960 * 10 ^ 70 + 1920463792836276486236914676195733111714617353807067637737349340869458) * 10 ^ 70 + 9174332995540809213368092642353287041274252065254748408895884411906027) * 10 ^ 70 + 866963860266218171969102372299429224131099737696525223054808158480701

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_390 : Polynomial.coeff recurrence4Scalar1Exceptional 390 = -(((15950409903695678086309350749367587075341878944748123739263689 * 10 ^ 70 + 3475033184019640231267909795629433883817878398484061373333631380528313) * 10 ^ 70 + 8479297987857919046197892547228729119607838949670862796791016882486678) * 10 ^ 70 + 7674737228517269877511038678728552595934623668995249856812848824642686)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_391 : Polynomial.coeff recurrence4Scalar1Exceptional 391 = ((6749068036211538135355156281893148884226522184938340937914293 * 10 ^ 70 + 5728188117065275114597780679870472125389929722197728425329659081008906) * 10 ^ 70 + 7155599785832981553566438045708701225348712898678680280882132395320901) * 10 ^ 70 + 6224617910776668476006338712970095085925584986722921487340776848699823

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_392 : Polynomial.coeff recurrence4Scalar1Exceptional 392 = -(((2812097454699148755030244344210908242622591130220696886861262 * 10 ^ 70 + 1612670798806859976907144112318380124964379844089854808315837801935731) * 10 ^ 70 + 1465906036972355535274850926892661569355286550808964872583422279507716) * 10 ^ 70 + 1253236322711841212308012437641220455729717916334004113498244229794180)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_393 : Polynomial.coeff recurrence4Scalar1Exceptional 393 = ((1167508782700760428990236022923987059475103829507433771557614 * 10 ^ 70 + 2506092633129738979269848601037946097168348491312592337397786845773661) * 10 ^ 70 + 7954601248695758351476621803835260755438416173354459875522181236785279) * 10 ^ 70 + 9171927425296381123978548741824246161173725724100629536855980707242527

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_394 : Polynomial.coeff recurrence4Scalar1Exceptional 394 = -(((483232701264813798914485859767888130717615162013252797601275 * 10 ^ 70 + 8213598442290321024949351491794927659936195002490855201712660704596099) * 10 ^ 70 + 4877003871660107837733210418187282239955844509348758020150685392555925) * 10 ^ 70 + 1706740951502540143340778617940315100297343555658756960360560758465600)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_395 : Polynomial.coeff recurrence4Scalar1Exceptional 395 = ((198090029114758334508239851271728799073753482575901476307986 * 10 ^ 70 + 1019715693022081584456395069918918928860510594416466745091562360069158) * 10 ^ 70 + 9355388090583531335351290283850976051722807006044568939067686103758277) * 10 ^ 70 + 5110119842761599537868946176026669224702271514401195508688353171166130

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_396 : Polynomial.coeff recurrence4Scalar1Exceptional 396 = -(((79670455423483430195956625041008404164217623779414909557455 * 10 ^ 70 + 3403123524699332612647668189729802088963453623417050980605818809778301) * 10 ^ 70 + 1697289824363104489225032179812866007651781168177305963548212367024615) * 10 ^ 70 + 5014280789984756328891191274309603393496204592793404157648221235374141)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_397 : Polynomial.coeff recurrence4Scalar1Exceptional 397 = ((31148936114351143779523336349895476260802275958578472945924 * 10 ^ 70 + 7971144893327991721886142237555725371571769044100307626226632465160393) * 10 ^ 70 + 9017208476858306702250165013850714260764096297792044377756542105589824) * 10 ^ 70 + 1312079296819735717140170563125046095172261349539504544118725340416593

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_398 : Polynomial.coeff recurrence4Scalar1Exceptional 398 = -(((11745851069092318826691147466045146789116248142238925341026 * 10 ^ 70 + 6794146143778789648590196855715287549516533864567559573195394394194340) * 10 ^ 70 + 3887522263004406086311485621108978586375213857694885351637110576591191) * 10 ^ 70 + 8902693689372066308954616926431288836511638821783787813227299560489370)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_399 : Polynomial.coeff recurrence4Scalar1Exceptional 399 = ((4244204792928496231223755071523777979818138978616505889207 * 10 ^ 70 + 7670442362786982438664149306620914925081370237389859627611712436659483) * 10 ^ 70 + 2984518083026643781722454734074422665965007029739365075022321110031113) * 10 ^ 70 + 8854067150225596069651180181047615035660207494336728284830634227820641

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_400 : Polynomial.coeff recurrence4Scalar1Exceptional 400 = -(((1460995379549872475324477146351913532368582916210552387490 * 10 ^ 70 + 8182378455548834641372145809905660764009272284921862293769625267162101) * 10 ^ 70 + 163759469861653985423240209162041987425618446291414939203026611758021) * 10 ^ 70 + 7491809899251011783729584008672550233623527230439288172727610437960868)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_401 : Polynomial.coeff recurrence4Scalar1Exceptional 401 = ((476158767397510520417291522012505596986784077388263652758 * 10 ^ 70 + 177108740448042302402580698241252808403348124202158349149198529137353) * 10 ^ 70 + 1922988590241405690323955414478244566913385387840573870750639769071035) * 10 ^ 70 + 2290878029136809663406173444098707349875534803145699148772762617275455

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_402 : Polynomial.coeff recurrence4Scalar1Exceptional 402 = -(((145743465415009079367871029961368591399887008269734445501 * 10 ^ 70 + 2405507238632435742689008141954365977728185958878670066761274037711984) * 10 ^ 70 + 2624182019829749102273156148485707366231983872720499205449207442024031) * 10 ^ 70 + 5436120589563663061317867677099845546830349144244814746548083356994008)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_403 : Polynomial.coeff recurrence4Scalar1Exceptional 403 = ((41364510424055712668552156912283877525975803253779221195 * 10 ^ 70 + 7145953159406364356980113032208464030308918977468629258556813663637889) * 10 ^ 70 + 8423042651996887247654100736394608752067494428433162136943092295790599) * 10 ^ 70 + 2645637555604257095218304127850604673720187687807951750698668103333985

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_404 : Polynomial.coeff recurrence4Scalar1Exceptional 404 = -(((10630890357628869573997189333586264742675125450320083796 * 10 ^ 70 + 4708911013415797979635283994625587040185285376615526246175552002977953) * 10 ^ 70 + 400590089619595385792239703239287382458138646596646443617469118879785) * 10 ^ 70 + 8904752320755130127289299842391587158054496460537990470757988060778664)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_405 : Polynomial.coeff recurrence4Scalar1Exceptional 405 = ((2343834116191918205561012511429857709108871600208225104 * 10 ^ 70 + 3586357411997271169538165696263333601606843448134657018740414057367522) * 10 ^ 70 + 7881847778726366785766898299813245820452224190187339873888106920420808) * 10 ^ 70 + 2820587090078780963926584183607916899355478175140953023494905764895857

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Exceptional_coeff_406 : Polynomial.coeff recurrence4Scalar1Exceptional 406 = -(((371140757639016852764663525729249864289555874711150941 * 10 ^ 70 + 9966175715641742511316845465087101886259690467622264561106914046912438) * 10 ^ 70 + 8679901248336225841123113254820655826435845608959817899105689875719249) * 10 ^ 70 + 3219981570483710761145893040672001848780314381172956675346187872106210)