Recurrence 4 lookup certificate: Scalar0Main 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.recurrence4Scalar0Main_coeff_356 : Polynomial.coeff recurrence4Scalar0Main 356 = (((86817777 * 10 ^ 70 + 8954950981549628137956439807066741889102750274680080519148387174815189) * 10 ^ 70 + 9514734048394909954412287330491582967143838428015875724154764399964968) * 10 ^ 70 + 2560396084874305998363983090417681580989943355761278885035556281938350) * 10 ^ 70 + 6381856991115585933703222764348845172602076481129002706618942870179461

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_357 : Polynomial.coeff recurrence4Scalar0Main 357 = -((((31026983 * 10 ^ 70 + 4800364359871912782344399177865246359593062432037677804061020968624060) * 10 ^ 70 + 960637257279215216425186783290862135664576501032448322858915011219460) * 10 ^ 70 + 2985757320888975099430641665295049952360511405419271359395034666465468) * 10 ^ 70 + 7174343467056545794493366952473984231128803547024742684260503546142732)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_358 : Polynomial.coeff recurrence4Scalar0Main 358 = (((11016203 * 10 ^ 70 + 3988573795974548584156792270876105613110577578946033839597055467798937) * 10 ^ 70 + 767708382019161306225360560265620314352254748033018356072165645387193) * 10 ^ 70 + 1812027294977065722568450561740280422006376903080705577401963404088348) * 10 ^ 70 + 610701464490053904882199018158923412488664465065920779248706393341470

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_359 : Polynomial.coeff recurrence4Scalar0Main 359 = -((((3934907 * 10 ^ 70 + 8149303587260610871543958977955093097933629599291402614833755533265509) * 10 ^ 70 + 4397036240390748436279046004067378733532690119625014440847244562021819) * 10 ^ 70 + 6006985120074058907708922965308583894002932144556129998969361892367061) * 10 ^ 70 + 128076775502678110620710704551554766711367262994462177020728815464415)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_360 : Polynomial.coeff recurrence4Scalar0Main 360 = (((1438774 * 10 ^ 70 + 9048902636336278682057297807610159268098102156713395240045741687468530) * 10 ^ 70 + 978620083032779338198297652609020805966066218845231101998312748521879) * 10 ^ 70 + 3454228838314298677357293589823696671090800669626379676948850736377894) * 10 ^ 70 + 9454557113911959096444842918359661164767677923151727566995373172802422

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_361 : Polynomial.coeff recurrence4Scalar0Main 361 = -((((548895 * 10 ^ 70 + 4886840600120930603072490222752051714313880442998589514864208017398671) * 10 ^ 70 + 7953364855459157685814978315428705703431075601781628630039277167199207) * 10 ^ 70 + 8001545116760313378379453613713947095261319894470672863151844077869176) * 10 ^ 70 + 850902783797091301564715723962521711620165979570996158643912725831192)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_362 : Polynomial.coeff recurrence4Scalar0Main 362 = (((221477 * 10 ^ 70 + 1608583835835543994874767835713894871336483324476142781097969970346719) * 10 ^ 70 + 2524008350596761728068630145639654432799530498150981784305353604052905) * 10 ^ 70 + 8857858388705235258489645962693060764590333532081130143210317439103345) * 10 ^ 70 + 5157451304080360975632087686193347167042459965764858158036631685807696

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_363 : Polynomial.coeff recurrence4Scalar0Main 363 = -((((94597 * 10 ^ 70 + 5385548805230266163526879489323997917321038203256417685105743444746155) * 10 ^ 70 + 163237510881984212142676638730689407995679392910734156240961676003993) * 10 ^ 70 + 510630148828198494205705493714535581642181035542082397395523780621487) * 10 ^ 70 + 2815924918433782522240126455229321591747667443587532737159550439924180)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_364 : Polynomial.coeff recurrence4Scalar0Main 364 = (((42237 * 10 ^ 70 + 6813375783286628931446815012402746384410361918175762317076216616144747) * 10 ^ 70 + 8549191800672455405192536906977504974725593559484973979618665366579383) * 10 ^ 70 + 2786933633264184444091971270454378925464983725282029300380181173060173) * 10 ^ 70 + 2277787735499585435982099880918735284534768465584469192909697083387365

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_365 : Polynomial.coeff recurrence4Scalar0Main 365 = -((((19338 * 10 ^ 70 + 6971930512623973843235404786719410393588506407832439926537815855052215) * 10 ^ 70 + 4064543985223639750577769357889875465022142961257991042375373972989969) * 10 ^ 70 + 2812816302462086576175281497439740440992450349039233092072165157822952) * 10 ^ 70 + 1025222667636709538171888779578382630256330534497505323321035954100685)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_366 : Polynomial.coeff recurrence4Scalar0Main 366 = (((8913 * 10 ^ 70 + 7545662282974860960444894983572200675966565794269436441426704531516339) * 10 ^ 70 + 846295603295231712680562772098055027617702677162511966486111009449027) * 10 ^ 70 + 5437419886628727821678389320988104317433398260040006061178768712456037) * 10 ^ 70 + 9199769256002685092136276970128442549357476121953262468808718949543991

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_367 : Polynomial.coeff recurrence4Scalar0Main 367 = -((((4079 * 10 ^ 70 + 2752023758817631471124325993741224781313071319093214145610016557910239) * 10 ^ 70 + 7275515123803274658448495167209073566444828782009495328843533257613880) * 10 ^ 70 + 3941011145467333722716724813350494462733554568302542350080557108430505) * 10 ^ 70 + 5036753566377025152374023522972452696276398081734617364358462386315886)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_368 : Polynomial.coeff recurrence4Scalar0Main 368 = (((1836 * 10 ^ 70 + 7898854074692374760499096834242856541270875795729345559648850661204739) * 10 ^ 70 + 9595710068450322088999517306883911588174119136220509125449728592854935) * 10 ^ 70 + 8887391378609599499020446074400738967352817236804688581531779177512877) * 10 ^ 70 + 8946451144818961365756475687109499388418464135820732492151688733546795

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_369 : Polynomial.coeff recurrence4Scalar0Main 369 = -((((809 * 10 ^ 70 + 3036812085094288825408528538373952476749516880038679747546771631423438) * 10 ^ 70 + 815753809483302331999980476556129235373831938375667144419397690528059) * 10 ^ 70 + 1569546556756747990712760367352563409888905241537249341565391624500272) * 10 ^ 70 + 6145056349660602855041865787282531658351481747392080619166722528245867)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_370 : Polynomial.coeff recurrence4Scalar0Main 370 = (((347 * 10 ^ 70 + 8102790221713256907965793014286000885518425461071094268599638829383985) * 10 ^ 70 + 3483469979390542990438489245479958905370199862511004698718517002458220) * 10 ^ 70 + 1820137364411935735792900186960479955397732326303371148881640953900495) * 10 ^ 70 + 4442008127607657952157007273027815680610653129492039505847266393326429

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_371 : Polynomial.coeff recurrence4Scalar0Main 371 = -((((145 * 10 ^ 70 + 5136983548985616439773869448647781041232238818429159695473345881529601) * 10 ^ 70 + 1024903065897330975384458409408462582064702879933053826923934935537618) * 10 ^ 70 + 8435413280491767523977036200422661175579805128168772126257161299985247) * 10 ^ 70 + 7878876011639211629953047511503783691993486114684204119752264709560389)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_372 : Polynomial.coeff recurrence4Scalar0Main 372 = (((59 * 10 ^ 70 + 1845835697000199566246222650535187560405476487370633737899187346774586) * 10 ^ 70 + 8172308732227895295135171454862672426866828218672435296729733978545200) * 10 ^ 70 + 9916592645380503582325475071585150892047650599363340673287661319302020) * 10 ^ 70 + 2775942522676288804991956347787226724525198345723818694052061006201472

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_373 : Polynomial.coeff recurrence4Scalar0Main 373 = -((((23 * 10 ^ 70 + 3746565372976844637875094509436168818117986771914968483880337807084888) * 10 ^ 70 + 7090919261192123839033507273248235673388125976801108525363050211944708) * 10 ^ 70 + 9787589271542753107368963948382817800834421325898614502678634623601190) * 10 ^ 70 + 5043023440430044446933683818383072050941701202723594443304808350505821)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_374 : Polynomial.coeff recurrence4Scalar0Main 374 = (((8 * 10 ^ 70 + 9526664646167444243456093795719448112889969181972374416246908429726172) * 10 ^ 70 + 5309230204493360664301737086492283617252918575792206592671007199877425) * 10 ^ 70 + 7102940207951848717667884668351976336302601438070265126799231468061967) * 10 ^ 70 + 6758511884035559182820556055399358520607476418044555856382200535699291

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_375 : Polynomial.coeff recurrence4Scalar0Main 375 = -((((3 * 10 ^ 70 + 3198400663202120789430370934551176044939855812247734793882809514044735) * 10 ^ 70 + 2334985682056750234278811772430545495028000624252436419965484925205217) * 10 ^ 70 + 6540079805174680815890980832076945568905548618904796070800502579782492) * 10 ^ 70 + 4955042861466142982009108225285506646445278070392409364209278729678238)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_376 : Polynomial.coeff recurrence4Scalar0Main 376 = (((1 * 10 ^ 70 + 1892389672131221373420889575136431863871924484551316096483870067259501) * 10 ^ 70 + 2845704385100516050737332072330428467841031828887914226129525916837139) * 10 ^ 70 + 5414671335338814442466148935622423151963897137085078204882012682626819) * 10 ^ 70 + 7434775678244587355610457913895226351451073859112205793976952962612390

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_377 : Polynomial.coeff recurrence4Scalar0Main 377 = -(((4102395532120988597787973335889675844147300720913617804590064372549479 * 10 ^ 70 + 2350986129453971493003672770607718490729341771283064050267791453738237) * 10 ^ 70 + 3621737617783246129759292336976214950509724999733962563652809202258136) * 10 ^ 70 + 1131849130226505121155869106186917345375518737920641984472049870759134)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_378 : Polynomial.coeff recurrence4Scalar0Main 378 = ((1356498849236387219643863683408073600916978266096071928183675445804393 * 10 ^ 70 + 1570606101830412704239632805697314632613374413979466131963695830420768) * 10 ^ 70 + 2283932716028855790597432547939066193682018495241414123773103189638209) * 10 ^ 70 + 5190920610274325792856114318426973626037290508943415702625857813471374

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_379 : Polynomial.coeff recurrence4Scalar0Main 379 = -(((426926479411988371335713978364365155336898909614092662300620419906260 * 10 ^ 70 + 260217224011836870322973515729335894825185019568873055078346709861231) * 10 ^ 70 + 6652286257489920442468680153494932440769233687608996280460895635028051) * 10 ^ 70 + 5237827171527076305213736865894267401478800258998759930251040722226186)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_380 : Polynomial.coeff recurrence4Scalar0Main 380 = ((126425839264600679549290788649364149445025938433354032346775784995028 * 10 ^ 70 + 3585553372619544856673536925399452707751563740152181405614940274068304) * 10 ^ 70 + 2679579278821760805328157339740864010260116935056430066175451633184360) * 10 ^ 70 + 6076632598532073284265036643501545089183328713591903916368725713442824

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_381 : Polynomial.coeff recurrence4Scalar0Main 381 = -(((34500375115173718255447611419259543872753238813104500157137967819972 * 10 ^ 70 + 4159200569899468192056769467922287417832412426194950606053006256897303) * 10 ^ 70 + 5497210532912023737575041964081037378249860077303292525197514695384118) * 10 ^ 70 + 3551243522259414305429278409743236579561730607347116172923242117589865)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Main_coeff_382 : Polynomial.coeff recurrence4Scalar0Main 382 = ((8300165323055698318497837719642105651547265048953959612392965888536 * 10 ^ 70 + 1117206982775338532043212479412455632169908377914787162568982290066331) * 10 ^ 70 + 2851380662904930025291295909540016782670581370842682479572766269243305) * 10 ^ 70 + 9277694672775719683117702887436594933129400884655880086636695631336037