Recurrence 4 lookup certificate: Scalar2Left 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.recurrence4Scalar2Left_coeff_358 : Polynomial.coeff recurrence4Scalar2Left 358 = (((12043 * 10 ^ 70 + 6556518629185866869501035774644703588126853730127602773433150891344950) * 10 ^ 70 + 6221097494299367500788902185686813152520538147623196826277446801393198) * 10 ^ 70 + 7128265260743550268223125817285502597788024279696718259325141166700404) * 10 ^ 70 + 9736614336906760950662460494334116265508374074560393571575239684262124

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_359 : Polynomial.coeff recurrence4Scalar2Left 359 = -((((5211 * 10 ^ 70 + 5783449676338926003671025949423109776620569834192310918716042959419761) * 10 ^ 70 + 6733759921425597107504417077932855622539705197822247312059584499873843) * 10 ^ 70 + 3183688369903599110656011573902367000882272210388839371457495231737720) * 10 ^ 70 + 274576872609415898054943841711285137527647311180343664870216200195120)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_360 : Polynomial.coeff recurrence4Scalar2Left 360 = (((2295 * 10 ^ 70 + 5017403577585325968997587267835639510921476134134937890674127000271525) * 10 ^ 70 + 710669389098572363479702337235768982436845282050721021988760563844468) * 10 ^ 70 + 4983757696670666767648224690883477999522820963810474823980244272814445) * 10 ^ 70 + 1656784918600268077407247158793829112843899225327658204598453219268695

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_361 : Polynomial.coeff recurrence4Scalar2Left 361 = -((((1014 * 10 ^ 70 + 7978019083690633855934541189092438799209635409078036274822612081088472) * 10 ^ 70 + 2230489234911899651915703482283069656908531569275564924895493655745071) * 10 ^ 70 + 3436066645181344145632299149770365949499630111689939072826594126046231) * 10 ^ 70 + 8924909021166182266469524088791242831157556641070197014638748574655682)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_362 : Polynomial.coeff recurrence4Scalar2Left 362 = (((445 * 10 ^ 70 + 2741306940391640936443187047047986364583304743296181734549318809601295) * 10 ^ 70 + 4318807172365869449889001421689267795330471009072835683894262669271517) * 10 ^ 70 + 8817002538248207661147667002962030328257733107439152730658322036026815) * 10 ^ 70 + 656212200455836257338957266941622650974701062326154512771855881509388

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_363 : Polynomial.coeff recurrence4Scalar2Left 363 = -((((192 * 10 ^ 70 + 3849661992547868419115317086099079828883706109385286164938981736486937) * 10 ^ 70 + 2526622803563029499974508615911859772348283492973937463845702477972250) * 10 ^ 70 + 4622855130995696818649207436881280968891751438623551109278898515101975) * 10 ^ 70 + 2104356938620115276189366289960009931651919458700119669202805775656356)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_364 : Polynomial.coeff recurrence4Scalar2Left 364 = (((81 * 10 ^ 70 + 4078339967504007025613402986351200055623605261736528480012737804743709) * 10 ^ 70 + 4483196694852692373534817578931546302592703185843090725011331482023178) * 10 ^ 70 + 3778625026076295692550605895207637119367287037350471197751349805671632) * 10 ^ 70 + 1055231874087363795547465973162723701637892886823349399602504969885890

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_365 : Polynomial.coeff recurrence4Scalar2Left 365 = -((((33 * 10 ^ 70 + 6119854956930676053467310186540363294830532928252158921031942006626845) * 10 ^ 70 + 7202474460510206071652097263330703600521137451052875805839036552733691) * 10 ^ 70 + 9025736547435331906314721948413001674632845013314709722570770291946564) * 10 ^ 70 + 5330706549034378209466606872004476784230228804941187705171944382769190)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_366 : Polynomial.coeff recurrence4Scalar2Left 366 = (((13 * 10 ^ 70 + 5031031152509680885076665397952208769869152265085176599007357457410167) * 10 ^ 70 + 6025790413275275051335936082828369511514313525384947832284053626726709) * 10 ^ 70 + 1619706198737147020597589565358352223773155177051683260079473977163430) * 10 ^ 70 + 5157023591510315900823476631926158682826689843030109990303745316567536

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_367 : Polynomial.coeff recurrence4Scalar2Left 367 = -((((5 * 10 ^ 70 + 2650758452128127990591477210079870008921422030434133610398439724935005) * 10 ^ 70 + 4875759883757176667125304634578093779142894345720632152646653856964275) * 10 ^ 70 + 9094437294095989323356658524353553760444972480092007255738767633424026) * 10 ^ 70 + 2239973372937932376653249930291508369928439082290613854866232057965906)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_368 : Polynomial.coeff recurrence4Scalar2Left 368 = (((1 * 10 ^ 70 + 9872944010922312640049805449741488881686473548242190902452667585912351) * 10 ^ 70 + 431524830827308311859621119333237231749794716377082388572160057288763) * 10 ^ 70 + 92985510879364924665460900285979889091144189333148713401623309807804) * 10 ^ 70 + 4965824740768683699796343149474145611857940221329754854252288261356353

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_369 : Polynomial.coeff recurrence4Scalar2Left 369 = -(((7237627219924316758240999093847130562675512904442786661488826066073317 * 10 ^ 70 + 9844339800499341574789052924578807171394900970027547305578037854761776) * 10 ^ 70 + 7153320071409854778521751038736849271615139741074372078342394438614478) * 10 ^ 70 + 233085533087188062966432564092811651940738670473304565663471917510515)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_370 : Polynomial.coeff recurrence4Scalar2Left 370 = ((2532107001458735218233426333418257551562942610458790829506328832251209 * 10 ^ 70 + 7883261115552533682897812289813947194307130641150924032070265915621310) * 10 ^ 70 + 1525054218198579930904017471706339233637652116030080756869191314672343) * 10 ^ 70 + 1414646718776183755224320110622649125363981457621359411631474264862341

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_371 : Polynomial.coeff recurrence4Scalar2Left 371 = -(((845442830063413075816568544619864117975339135820966606651426004511198 * 10 ^ 70 + 2602863205789381369285718354558999456185606610988135721949766543246295) * 10 ^ 70 + 7745901748340681741024682064025945866414211663158859320735707356891700) * 10 ^ 70 + 3923271155719686037041484362327253810500807621140466725327008639802688)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_372 : Polynomial.coeff recurrence4Scalar2Left 372 = ((266624086400572999466762802171288119734871953662569997232675637371919 * 10 ^ 70 + 8635605916535715253743955725509130051261021263946753961439263937673222) * 10 ^ 70 + 6818178253761103234732272941548349500104779396482089270886694080381021) * 10 ^ 70 + 541280819781116805137673046038407274939870750140616460556385748034755

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_373 : Polynomial.coeff recurrence4Scalar2Left 373 = -(((77993153632536626698132318789354820438086140147700221283179306289541 * 10 ^ 70 + 6104388011871569511173673788214496577079269220680590320350714044181624) * 10 ^ 70 + 9048952641639761676248193630978276992417922063807681274220236041019681) * 10 ^ 70 + 5359399106566570639021349011774671580273068290678255695253454264726756)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_374 : Polynomial.coeff recurrence4Scalar2Left 374 = ((20402058429805995741326034053663442433163762638152704925343951345434 * 10 ^ 70 + 7612654696045746960024928909384207805643046644885627311109203032258489) * 10 ^ 70 + 4960483949565711033794310187377292678090284083118687234289570780803053) * 10 ^ 70 + 2858436258877479354764842032331496192181194715461099899884695490874644

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_375 : Polynomial.coeff recurrence4Scalar2Left 375 = -(((4340494595323872933405731236412059215489818133412365210975447469390 * 10 ^ 70 + 7534756628951527008351165765278097248315830720381980552299056587442574) * 10 ^ 70 + 4494981316551390013427055889072382741386028976154831485799666137705793) * 10 ^ 70 + 2808918833994892054094194137081322417625235429396231682816202703588956)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_376 : Polynomial.coeff recurrence4Scalar2Left 376 = ((474835163355693534283140736112441330939213135558169069111753726072 * 10 ^ 70 + 6443563528407296598750615119733101142206689195900749792998077259071023) * 10 ^ 70 + 5786043666434337619129342047892776436186764805816792851223155797070252) * 10 ^ 70 + 5316315302003189268526526085655099137164746396804404505080644216474066

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_377 : Polynomial.coeff recurrence4Scalar2Left 377 = ((192501557472663112437242973522048199753360588458535533020615330303 * 10 ^ 70 + 6707585182446764172379488969781912350704891934642435561054079690621398) * 10 ^ 70 + 8145996032611948038227766659438211549273651065015723144663000236629258) * 10 ^ 70 + 7001412334851814534077417014733800196804453199839857261685737902591442

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_378 : Polynomial.coeff recurrence4Scalar2Left 378 = -(((179751563990354565683951421900542797030741574926043619570717615274 * 10 ^ 70 + 3335311186787572088270980624663552937600095487538728126737691614131609) * 10 ^ 70 + 9145649224162915951961323628208841717096026780519267747105053791795480) * 10 ^ 70 + 7511095467854256704842548640726425288681761418433856079650320382764595)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_379 : Polynomial.coeff recurrence4Scalar2Left 379 = ((94089626649466921790199605853446777730752719464261377265272035485 * 10 ^ 70 + 9488828765762464953444900914057690778348594163213960277292878897888234) * 10 ^ 70 + 9282421753213986763232373393996374002050927610820147957267594131668165) * 10 ^ 70 + 4756859859936874087745248375858815261020886286880613567949656691034530

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_380 : Polynomial.coeff recurrence4Scalar2Left 380 = -(((39964513516020553125674109062967332874300021919390173970408172948 * 10 ^ 70 + 5700906607580028422519978163702835367894256968521201214262261692254988) * 10 ^ 70 + 3551340471543154866670325169965504915535152060798031875883923390723881) * 10 ^ 70 + 6310890606239748203839640482162927502269131597788118142709823554032587)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Left_coeff_381 : Polynomial.coeff recurrence4Scalar2Left 381 = ((14848382274503983674175699377434665843394195652975028826933129746 * 10 ^ 70 + 1850366721282398402001718189730906455271559244402248764715598138049562) * 10 ^ 70 + 408510122637230977339211419268040309268153787792870282449552984152876) * 10 ^ 70 + 7618426632079211494880629542242499929230371858387251820639207575437956