Recurrence 2 lookup certificate: Scalar1Main coefficient convolution

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_303 : Polynomial.coeff recurrence2Scalar1Main 303 = -((6450090432958324587763034404741638943435917136470162 * 10 ^ 70 + 3934587375121175080553305079829883394160625165373738511616364579950194) * 10 ^ 70 + 6021867118322284325924735198101474796941419553616292984403930491011130)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_304 : Polynomial.coeff recurrence2Scalar1Main 304 = (5779203274871504473939480306201448418446151879824757 * 10 ^ 70 + 281507904351783158683462427152990502464927536668617057469804771247952) * 10 ^ 70 + 6826250172240601142521554916483819676306087803890209474277751880041436

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_305 : Polynomial.coeff recurrence2Scalar1Main 305 = -((1960119551363546757334708467579131794528099106029179 * 10 ^ 70 + 1052482829963891501574550201682484389892726580272937112962034650279687) * 10 ^ 70 + 7989602638618267317018232545657641060622081527313565269751450003165647)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_306 : Polynomial.coeff recurrence2Scalar1Main 306 = (487530779654419217619530951968461404561952780095391 * 10 ^ 70 + 2843722737743558849765877642771252781798727241519159943255192407939191) * 10 ^ 70 + 2989582547237962774031339165413171833243876775048655547340405175935386

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_307 : Polynomial.coeff recurrence2Scalar1Main 307 = -((97381771249800552550954307910271117917636268625635 * 10 ^ 70 + 5175682608372888167581598777280739113217642032445638271438431312257082) * 10 ^ 70 + 8527149068576148004947292855684791312628927956103256944293185171264654)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_308 : Polynomial.coeff recurrence2Scalar1Main 308 = (15526669165083472395213059560437249814462776306812 * 10 ^ 70 + 9329315590393787341178820240622761958476994926426677715538729854612010) * 10 ^ 70 + 7964789142308388162774274690397226753622642275591187980671969802684922

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_309 : Polynomial.coeff recurrence2Scalar1Main 309 = -((1761758718206354150811781856917563926564047664781 * 10 ^ 70 + 1282775080311451220727910957761084266283733623067226186097510060542360) * 10 ^ 70 + 1040900245243167613611751049845608145895458610702247027056267509796955)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_310 : Polynomial.coeff recurrence2Scalar1Main 310 = (51889744475777608265718376166839647651324771617 * 10 ^ 70 + 6244749086127005623999589739430759050356976980058179148384220558140851) * 10 ^ 70 + 1863081118749568162393419569613337087450270683701780259570907889460267

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_311 : Polynomial.coeff recurrence2Scalar1Main 311 = (39697730346914821578828751706281904743102294744 * 10 ^ 70 + 104420639052907017638726598927370918981279143568852677384193642836267) * 10 ^ 70 + 3200340306824602375928150631777814822781591599086743967747645094139430

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_312 : Polynomial.coeff recurrence2Scalar1Main 312 = -((13740159818404412443750336707627252654376481891 * 10 ^ 70 + 7173153335649494147433970032764270436260290331906881642065710677087567) * 10 ^ 70 + 6197616830811000195466475612699265613454036096166917039780817573788622)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_313 : Polynomial.coeff recurrence2Scalar1Main 313 = (2962589837468223407070800093653755900873713111 * 10 ^ 70 + 3259429362745553878574727787281863209551969602156986574601133418815643) * 10 ^ 70 + 5341434931026278631650400298190632564042667803149842187181014400283527

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_314 : Polynomial.coeff recurrence2Scalar1Main 314 = -((488532780767606520620876953641486171914405710 * 10 ^ 70 + 749624536758118943187565534203156455170024609835047450948971211637632) * 10 ^ 70 + 5918286226627246754646297745477418860075956000476987842892965310214365)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_315 : Polynomial.coeff recurrence2Scalar1Main 315 = (62714800952022312916902773459548678281726704 * 10 ^ 70 + 7461036309433402696665914950938834358706237302834480563762374041478087) * 10 ^ 70 + 2335124832783051490207250094742818840495732456724487037362215026389025

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_316 : Polynomial.coeff recurrence2Scalar1Main 316 = -((5660200639059507616012700337427189414307150 * 10 ^ 70 + 2059340125820341101436318460976235454078214320361376637828168349019771) * 10 ^ 70 + 7879327779993741476432555353245749907344505703564527997972474652925888)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_317 : Polynomial.coeff recurrence2Scalar1Main 317 = (149839267117240727819235554511159247146172 * 10 ^ 70 + 6675848433884798788605420731247501044750113174234868295508087387019129) * 10 ^ 70 + 9476956012255925523470781635427361346050127521036613266083058312893487

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_318 : Polynomial.coeff recurrence2Scalar1Main 318 = (68141227635070960871813531263733121285858 * 10 ^ 70 + 8912913332916002987297001969946227298522805075881863836763335217615562) * 10 ^ 70 + 5390425942868135704368207069214972547488153661336567810813397018937055

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_319 : Polynomial.coeff recurrence2Scalar1Main 319 = -((17745877016124153142133207449636719710407 * 10 ^ 70 + 1418428334734056946928120217232324878596885561277124012669990377591173) * 10 ^ 70 + 1405809034946984812853514952517067861045115801626132055342002450997459)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_320 : Polynomial.coeff recurrence2Scalar1Main 320 = (2721035712270283247121455316902967452447 * 10 ^ 70 + 661188888257550288129034058176364315444553527080332353544364869025948) * 10 ^ 70 + 6575347198000311190428550620040471330531594033144555103310718983491441

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_321 : Polynomial.coeff recurrence2Scalar1Main 321 = -((297755540244667526559078258933407676234 * 10 ^ 70 + 1918763956604527438483792991439667427263304748806487981384165010254496) * 10 ^ 70 + 2102553297114591141207355132495902314628796700167679384603450904270894)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_322 : Polynomial.coeff recurrence2Scalar1Main 322 = (21520026781288169721137337411521440650 * 10 ^ 70 + 6729277649679389439524771816101417319305313900197609689257160654499529) * 10 ^ 70 + 6737304271070186874378055726139175839032865212874220717573538891994351

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_323 : Polynomial.coeff recurrence2Scalar1Main 323 = -((312637191860920648293130885138634504 * 10 ^ 70 + 1876855675143147620934585298624244305877275629593915779122550844089138) * 10 ^ 70 + 854016782300778717430785936285158734960215544406314241731359089178967)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_324 : Polynomial.coeff recurrence2Scalar1Main 324 = -((190880915396306214883834881756756868 * 10 ^ 70 + 1540064885276574109173821912514475242013098991067761950561900723498381) * 10 ^ 70 + 1682617708696866995256421998731478459429167685960974865859905045974879)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_325 : Polynomial.coeff recurrence2Scalar1Main 325 = (35707040607585651452890159599162930 * 10 ^ 70 + 9777598571436802198328524369547868622608052551673978575827859267420718) * 10 ^ 70 + 2675766360193954204785699007036731769286616446963641443847640264326184

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_326 : Polynomial.coeff recurrence2Scalar1Main 326 = -((3936890612143167948971256628318076 * 10 ^ 70 + 4706339461649136878754081761776680222139649022052138805994501496260607) * 10 ^ 70 + 2790666993899646794605374926074523382688717635715000933914965675091938)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_327 : Polynomial.coeff recurrence2Scalar1Main 327 = (292315402242204107613833580340204 * 10 ^ 70 + 1529040197843110998902876566100975016346945782070937806200036431516969) * 10 ^ 70 + 8649507349264886326169926502411498378625200508757508907356366055802988

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_328 : Polynomial.coeff recurrence2Scalar1Main 328 = -((11425722820211379679141625522393 * 10 ^ 70 + 1671994518725692671475468407507195143068780952594004234855928347298899) * 10 ^ 70 + 6752150441232572056246642245491235610527873509412131936900669440079399)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_329 : Polynomial.coeff recurrence2Scalar1Main 329 = -((498823343028814528334612098291 * 10 ^ 70 + 8545009951455842001652544408366333115085813416447909635984951922500078) * 10 ^ 70 + 4871201852222330035791297604368267784298295410369168552247740884660316)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_330 : Polynomial.coeff recurrence2Scalar1Main 330 = (135644591992779898368916662093 * 10 ^ 70 + 6919506516512777901180375414370370650590976872750234051797274451269754) * 10 ^ 70 + 2439708364340796362718439604385167888297082022745955043048619761522488

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_331 : Polynomial.coeff recurrence2Scalar1Main 331 = -((13497670761367856140509916329 * 10 ^ 70 + 1271617766690670024868536899921931608193757847466653480645282265438183) * 10 ^ 70 + 4091012170048961823766732508272179486033708679855994398163704338110878)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_332 : Polynomial.coeff recurrence2Scalar1Main 332 = (846369700333953928080638897 * 10 ^ 70 + 3954111931563334943116072691116763339143695212180520944327074338203072) * 10 ^ 70 + 8815169096384878786120898254597894243582408101090500869176377826083924

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_333 : Polynomial.coeff recurrence2Scalar1Main 333 = -((30337230249787186777241050 * 10 ^ 70 + 5740050030174702955203262693385133802548956640029672225857572957978853) * 10 ^ 70 + 7104637694985004104758976958641751558806718651430656491238930966443927)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_334 : Polynomial.coeff recurrence2Scalar1Main 334 = -((200901537136208063037858 * 10 ^ 70 + 8647040227816484471691585714657020061684633771248356773251331529986035) * 10 ^ 70 + 1636294667682527947518357866611960632540366283649953612094813260870897)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_335 : Polynomial.coeff recurrence2Scalar1Main 335 = (111807098803629991193069 * 10 ^ 70 + 5415019703961389331742780602797157827891287531048340564653419436100415) * 10 ^ 70 + 9230882154840539868289169726868362079060136590497488743098647703976246

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_336 : Polynomial.coeff recurrence2Scalar1Main 336 = -((8283592157090366967221 * 10 ^ 70 + 3981555187239525042621952510612727754869659605164310575820582853654060) * 10 ^ 70 + 782272592265814375073648172117586101784273351350983604788386231458565)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_337 : Polynomial.coeff recurrence2Scalar1Main 337 = (341252410607635173671 * 10 ^ 70 + 5071741101327398071876430080521340359944885857146440339137630983564310) * 10 ^ 70 + 559286373056440730989116705452546347416535622808610970268489008946840

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_338 : Polynomial.coeff recurrence2Scalar1Main 338 = -((6420915478082712553 * 10 ^ 70 + 6602964471544151177256431182684673636592656703620292916704035137067886) * 10 ^ 70 + 4071726221715339578635237074351247719987411171617243214144582403126640)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Main_coeff_339 : Polynomial.coeff recurrence2Scalar1Main 339 = -((159406125514948132 * 10 ^ 70 + 6199001439124501867759353404754330637371014547048124980443077299915802) * 10 ^ 70 + 8886484717254362361506721606399045853294668099640834729603411111082112)