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_378 : Polynomial.coeff recurrence4Scalar1Left 378 = -(((5184395983769027852847002975524527465335438398369210784689856552893 * 10 ^ 70 + 969372309464475302362329823268433030290153067019765316649732349528792) * 10 ^ 70 + 453973447140284967636297861569172310567423085565869613184453143806844) * 10 ^ 70 + 7124178883419109400006002366099035409960334181266870312408176450720565)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_379 : Polynomial.coeff recurrence4Scalar1Left 379 = ((1129574478436834367573346175181540345481205775225292315384252215813 * 10 ^ 70 + 4052966580433267642352802924314420325687455892843420406748663802730052) * 10 ^ 70 + 7021661533654289894962659777807590008377719976423763810907234706024603) * 10 ^ 70 + 9694469115296107643398940286742351076086441462985708979940394080625717

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_380 : Polynomial.coeff recurrence4Scalar1Left 380 = -(((121028533019063157930345440651346071660720643912405470294585728417 * 10 ^ 70 + 3083963541625199905810592368894866889974586675012022347671867378100137) * 10 ^ 70 + 9074323685805730479602792767971815499254407851976569197385885503476452) * 10 ^ 70 + 5621474938178082636374540965488070614031256701757863897072206938364849)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_381 : Polynomial.coeff recurrence4Scalar1Left 381 = -(((57370426781855837064215306724523294166299451804097830848873450327 * 10 ^ 70 + 8339282265932822400134798879773622187031288722455061298772786270919433) * 10 ^ 70 + 6023875651488252622048826465761931821137809837042939113837989908779100) * 10 ^ 70 + 4061381243115326642976531694972105091344256056412910099518899356814209)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_382 : Polynomial.coeff recurrence4Scalar1Left 382 = ((53071550311904850667919256663173240044298243141606914121888554199 * 10 ^ 70 + 8928974368025116292605980061079042051789862443425425646299038009156903) * 10 ^ 70 + 2738696938288784368262468936816882507401645546517867500665539803737050) * 10 ^ 70 + 691511927651696380979764687624637321890489759315868738027083892143470

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_383 : Polynomial.coeff recurrence4Scalar1Left 383 = -(((28373442572871288916716120354684086660041860005961043450676951121 * 10 ^ 70 + 2931711969488744006667843482529092215975923862210579451397602396121102) * 10 ^ 70 + 3844910645073010935941938305439600112020506231819777091525269065087851) * 10 ^ 70 + 9338664821262804088342270539060307364671819712108424975579404691465908)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_384 : Polynomial.coeff recurrence4Scalar1Left 384 = ((12433804491818164754279297968569743303502533864650036922072997588 * 10 ^ 70 + 672778482156620383489685823236268885146967894049163077234454142790857) * 10 ^ 70 + 2329062131414605849176293182595432435550728363466334008864914487320239) * 10 ^ 70 + 1051454334660554200323763124930673969474249513841022938675308855372182

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_385 : Polynomial.coeff recurrence4Scalar1Left 385 = -(((4828268507577464980642994758652915296528556869432928374630319907 * 10 ^ 70 + 9426587182209432766775614418133439804650233359259867279787401573065866) * 10 ^ 70 + 6449905109542131585084477840051458950079451139658903261272296525880015) * 10 ^ 70 + 3878424037237267831153961690113460771430299774083651059126513988034501)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_386 : Polynomial.coeff recurrence4Scalar1Left 386 = ((1704657296331541867004462858263069939288770355168195292653901394 * 10 ^ 70 + 8876369418313651997991352263579688667112146997387044596426250883088184) * 10 ^ 70 + 722272668040573707220819359754722360072851046865943691157518014269714) * 10 ^ 70 + 8086856986015165128308425280075087185706333256432126508342454150057970

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_387 : Polynomial.coeff recurrence4Scalar1Left 387 = -(((549309722467978878782192371994894273102602364839814232070036826 * 10 ^ 70 + 3468015814072826144498516552546834959551441431356986678748966460203058) * 10 ^ 70 + 6451553485900429400697865066870211542647802351389675303951276314588884) * 10 ^ 70 + 6134327349850092313053942615630471545166586136439303904343202716145962)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_388 : Polynomial.coeff recurrence4Scalar1Left 388 = ((159044801147796498539819130957547826535642765947939561753948391 * 10 ^ 70 + 3286264525488206853040573960673176006567387302105641122614405868594700) * 10 ^ 70 + 583820797948522275307440059900121948081843425909844059006863301958072) * 10 ^ 70 + 8821946903214517660065174862898230876308880208386339601106378282001349

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_389 : Polynomial.coeff recurrence4Scalar1Left 389 = -(((39186692599032249784007704964570443393647130411825342329738358 * 10 ^ 70 + 2155067286111486523008971044143678755154030771580528282418916547588693) * 10 ^ 70 + 3609922060695214527616017017112027332843435912309189129142949938624960) * 10 ^ 70 + 5753112530640919655562018215253359411513640141776150162966726744169509)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_390 : Polynomial.coeff recurrence4Scalar1Left 390 = ((6666164835367861813806416252754550173595519766680834072890405 * 10 ^ 70 + 8737670743983788340784901529571715869199840831786667525714188297190970) * 10 ^ 70 + 9427332373990365355310332218147704565488073843874656944461940870901039) * 10 ^ 70 + 2858166820314306761183197505890032981286079049077701129565453092693878

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_391 : Polynomial.coeff recurrence4Scalar1Left 391 = ((425285582732186555249886375613842322910834452102880648297440 * 10 ^ 70 + 369241232486777157760068883591423045285253749233127255158744045489664) * 10 ^ 70 + 9953781810546924046497949020870048502172182079848795860872742463295532) * 10 ^ 70 + 1372496979955000489330548183391723710230598940463066258969426992181227

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_392 : Polynomial.coeff recurrence4Scalar1Left 392 = -(((1160734669988461042159423227241626333858937342506088582485801 * 10 ^ 70 + 2287449372526782385360626520119748752376995220343238625326536201844632) * 10 ^ 70 + 1567866262375381087126355900263776580925329374552993338413960302193333) * 10 ^ 70 + 2136284883350671346836528226681884750934471014308588787699761794841790)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_393 : Polynomial.coeff recurrence4Scalar1Left 393 = ((757595893636487519216804086458773780341110614856025204236657 * 10 ^ 70 + 5177781182653635235963376911462006898950775605353631441387683000666650) * 10 ^ 70 + 6691975986395714764396294304046122679979316823869030095849134053786600) * 10 ^ 70 + 4975231620311884438575256123616638534333065911311716828303004598004352

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_394 : Polynomial.coeff recurrence4Scalar1Left 394 = -(((380611221973894335048433900060036262726260755932085488796957 * 10 ^ 70 + 610956195486890569519556069200061290651811800800563018441234724164357) * 10 ^ 70 + 7129301570345686047505279929551860104870209103024622305794926185140240) * 10 ^ 70 + 6329742336751715360957571066200946475479399967095344398403379579287823)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_395 : Polynomial.coeff recurrence4Scalar1Left 395 = ((168761120057167439902959426670529331973435751681045480993932 * 10 ^ 70 + 9372540741892671232251622667024015384752722119403222205437319163920087) * 10 ^ 70 + 9123042979880710758760993049219083945350642491621829469175838235862265) * 10 ^ 70 + 7334600058053116707212243595783873658615520471064093077840035553849746

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_396 : Polynomial.coeff recurrence4Scalar1Left 396 = -(((69060869301597399130319385471724894682774498149922123458558 * 10 ^ 70 + 5566724593655040889708485522639918741616154997561828845336876830197764) * 10 ^ 70 + 8216671448291046091602163552679278130971896591011331631662386853224668) * 10 ^ 70 + 5294280310255789658869205245401863589341869579179241828513758968031546)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_397 : Polynomial.coeff recurrence4Scalar1Left 397 = ((26578454024554951720941904152035330131336076843503960620297 * 10 ^ 70 + 8246792037587459931949289660159761704056504474208641657321111702868536) * 10 ^ 70 + 4525490638814040889227238378510969934284150899244790369794594091320532) * 10 ^ 70 + 7184197815494275435890863235193019915984743390337233067805795836525019

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_398 : Polynomial.coeff recurrence4Scalar1Left 398 = -(((9698189262958152242946129365052065770013878725871103078798 * 10 ^ 70 + 735709450118316242150415941435016352296927257940633388330122710906095) * 10 ^ 70 + 2410527469200493932847479430898218317712074653768523576192763492501067) * 10 ^ 70 + 7933052813161163384304320872882457009998217115114619829595426526288015)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_399 : Polynomial.coeff recurrence4Scalar1Left 399 = ((3363000948392240711855007990001021931226596829920022450139 * 10 ^ 70 + 8770254419649893239200538792303394791800210511164294207094331689056557) * 10 ^ 70 + 1148887393247729445119288055183807771841084661582271649686966557815553) * 10 ^ 70 + 3845697504918753783685128126406923297535687922970223986177812389646568

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_400 : Polynomial.coeff recurrence4Scalar1Left 400 = -(((1106162699042217673750501143396859749393183937962724373199 * 10 ^ 70 + 6980409830882593221334563433959987330606650876951412561757954365823239) * 10 ^ 70 + 845542544506667950496252145360649549056863798192905226324350228800559) * 10 ^ 70 + 3364303269046946626067447422949346615713495613175190604015473541103029)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_401 : Polynomial.coeff recurrence4Scalar1Left 401 = ((342941454528929187117701649408725643606716506168835306203 * 10 ^ 70 + 7621491378997060510060937471391692777377105646302477243007545896470175) * 10 ^ 70 + 6141548473316803821434642884457392110685221355779128647736964202698479) * 10 ^ 70 + 6965953500615753657654902979656828476565452515934401428789910073588996