Recurrence 2 lookup certificate: Scalar4Main 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.recurrence2Scalar4Main_coeff_297 : Polynomial.coeff recurrence2Scalar4Main 297 = (41353634538388646484168953775309327911932753157465 * 10 ^ 70 + 6768017534665343513880172563974553695758934059851116922376802386623845) * 10 ^ 70 + 4857524707375061549368637572206401572230077117849303489070943896142531

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_298 : Polynomial.coeff recurrence2Scalar4Main 298 = -((4178386597069775943276381818568407501631973892778 * 10 ^ 70 + 871016405058339894084043169912028382871828185330322079167068754066705) * 10 ^ 70 + 4393371512530609575750703223781176525642711449913508577720870920967059)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_299 : Polynomial.coeff recurrence2Scalar4Main 299 = (5495389629105047772323408871684288551250643382 * 10 ^ 70 + 4990912986816103803140009333474642819237331465556376674930869766112279) * 10 ^ 70 + 8059523084146845173990818411456109494185380348918953372039236095889736

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_300 : Polynomial.coeff recurrence2Scalar4Main 300 = (135420193040473014640316302527284977584582788920 * 10 ^ 70 + 8487383494818866674684507660814388664057791564954015270901230210055264) * 10 ^ 70 + 4205484773822614885650738410985816383779927873843131024493947964518249

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_301 : Polynomial.coeff recurrence2Scalar4Main 301 = -((44104912937880438306714102322609069539732957015 * 10 ^ 70 + 9789224438193278484985191058122930521241913116947305435619471671472153) * 10 ^ 70 + 6192828427194851855331182625183348932967085702249845737496178306071310)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_302 : Polynomial.coeff recurrence2Scalar4Main 302 = (9911030065687357883971880177994653410723978869 * 10 ^ 70 + 1495051721109084210031271803826925776527891845508593831592329633967587) * 10 ^ 70 + 8970904228575958916249417772356085650247504127408416411492468342864358

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_303 : Polynomial.coeff recurrence2Scalar4Main 303 = -((1807837875328883515311356953975232434470126860 * 10 ^ 70 + 5975855266729791020101409256444092534458428335201604618282977623071387) * 10 ^ 70 + 7821883642888077850739329375583938567642018414438244109294451151265061)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_304 : Polynomial.coeff recurrence2Scalar4Main 304 = (278214221259425469815073353466747306421401896 * 10 ^ 70 + 1474044529714025445239379133550683751540696628725977650597189419420379) * 10 ^ 70 + 1005848501967200646628968781241451759677634455775010612747049945610492

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_305 : Polynomial.coeff recurrence2Scalar4Main 305 = -((36001291726442072894691218386979893021623602 * 10 ^ 70 + 2826499385966644845554732557004032103698199550909676243742757068642593) * 10 ^ 70 + 7251464760094997118420009156393378963966775100457827500847276361900690)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_306 : Polynomial.coeff recurrence2Scalar4Main 306 = (3738249621153094215332570364326009318342917 * 10 ^ 70 + 238407045485530254850719950465770606615890170069388003816817394042547) * 10 ^ 70 + 3198080371735786997526230605878210347864328235513146382052538186881950

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_307 : Polynomial.coeff recurrence2Scalar4Main 307 = -((259623903704500990260405745019338847096926 * 10 ^ 70 + 6968346729949074218682280952890458905741824704820655523469827980502074) * 10 ^ 70 + 7580866679276438736099906117810932651247780956368609651055466704847163)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_308 : Polynomial.coeff recurrence2Scalar4Main 308 = -((2132849371403927486171425369690421626401 * 10 ^ 70 + 8658958697265158244118438657351151258313158588906407742546131441526602) * 10 ^ 70 + 4237372731828779065928499942993326796778427790213618323657636581190165)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_309 : Polynomial.coeff recurrence2Scalar4Main 309 = (4511209689888116567068573121491980303847 * 10 ^ 70 + 1842625477204828575710598620328085541743100675189858196176485109616453) * 10 ^ 70 + 5206124459645712669996392154827478692823375662338773223585378952950105

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_310 : Polynomial.coeff recurrence2Scalar4Main 310 = -((934451341988013385458478257880226777721 * 10 ^ 70 + 1630035329982503793824302202823223959924948089558000019520207118137141) * 10 ^ 70 + 9662337566416448525233401291875079586459393960138986775091176856141512)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_311 : Polynomial.coeff recurrence2Scalar4Main 311 = (131533121507892038452257433473873566443 * 10 ^ 70 + 382638536200923565760520268913393670605585416157968953300075969516923) * 10 ^ 70 + 1924086595341852200610297960163147068253633037594278029320081945244583

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_312 : Polynomial.coeff recurrence2Scalar4Main 312 = -((14376442849084453212451581835818132249 * 10 ^ 70 + 9573884114612448688902343543476140198494669681072934329138547214222236) * 10 ^ 70 + 746225930029043287698656006872895261909110843464624724451451025722672)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_313 : Polynomial.coeff recurrence2Scalar4Main 313 = (1225733572854300844824537679597521087 * 10 ^ 70 + 6423882738037005593640432356299570788145604159590671028356979877753057) * 10 ^ 70 + 5452928774353253243522974226865294235583041602683223758255308811319143

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_314 : Polynomial.coeff recurrence2Scalar4Main 314 = -((73743440804838786042689531738145346 * 10 ^ 70 + 9806863091191908321598983972814180156545045353559272280304008084313935) * 10 ^ 70 + 2126363561733096139087453761996330890942070733499471895570766993059695)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_315 : Polynomial.coeff recurrence2Scalar4Main 315 = (1483746889143372936967617266352200 * 10 ^ 70 + 7120837758961503670764608238485808044988569419157913388197779454627161) * 10 ^ 70 + 926845726792911042249487642057694516881206052834197323041533458224340

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_316 : Polynomial.coeff recurrence2Scalar4Main 316 = (332582480285990071443916857406742 * 10 ^ 70 + 1305593223409146085944651657621160644035263336269227776764694533914116) * 10 ^ 70 + 7200483931009217934057778481577591881104865021563343301928125527424971

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_317 : Polynomial.coeff recurrence2Scalar4Main 317 = -((56763981880593889772840269087117 * 10 ^ 70 + 2179745440811610889416810001096638315443585638969011867797420040256379) * 10 ^ 70 + 3810290249793109250318575723568956525818335284263143947096802932632254)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_318 : Polynomial.coeff recurrence2Scalar4Main 318 = (5479833466758775103251105797054 * 10 ^ 70 + 8675852005104105992973486516233355860780878404211642235087686388192630) * 10 ^ 70 + 3452616986020674586663179501447636749468771853918854491889193249646894

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_319 : Polynomial.coeff recurrence2Scalar4Main 319 = -((372239508368341082421047320315 * 10 ^ 70 + 6985087570555715121665859279957128711913810767054561891877375031166736) * 10 ^ 70 + 2041058607401666932481501460169126564325896391555650545601122677142128)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_320 : Polynomial.coeff recurrence2Scalar4Main 320 = (16998012372980106747312856277 * 10 ^ 70 + 1280201506235855929756482292454308484243418362924543280058912482401222) * 10 ^ 70 + 6315657881828954242157746425863927522900264568298294902293752492853707

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_321 : Polynomial.coeff recurrence2Scalar4Main 321 = -((288339807445863622270916613 * 10 ^ 70 + 499337841502962510109618454030376307085495535065345012768528987271995) * 10 ^ 70 + 7002290528256837187585898887981748952978718643181823291910794542030761)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_322 : Polynomial.coeff recurrence2Scalar4Main 322 = -((31120484906599823554928476 * 10 ^ 70 + 1040518025787782052736833991013392152826777237575125218733511977394561) * 10 ^ 70 + 9240621523842011236245033881419214404851774773894506405669148750933216)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_323 : Polynomial.coeff recurrence2Scalar4Main 323 = (3591014601363149578121296 * 10 ^ 70 + 8885533394896063317182648242281788896594947796159024687451635786195366) * 10 ^ 70 + 2193867954339897215115631841294451208556785314367944299918503475805246

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_324 : Polynomial.coeff recurrence2Scalar4Main 324 = -((207980069907160280677862 * 10 ^ 70 + 4491986981157429276213093773451726206150125234273414714834335128519960) * 10 ^ 70 + 2059443460258599735080854967322409783074539660488603279019467135908906)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_325 : Polynomial.coeff recurrence2Scalar4Main 325 = (7317276666580844788248 * 10 ^ 70 + 3004018637408640347404269414755324093577357902725434712804390283068843) * 10 ^ 70 + 8598498251322792887645768632196873046284274516129464324429663285651151

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_326 : Polynomial.coeff recurrence2Scalar4Main 326 = -((100123225870060930115 * 10 ^ 70 + 5050939884059879197663912902062345361057442699106288220756343945673171) * 10 ^ 70 + 1566933128866222282056072038487854926660315901477765279155561919543939)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_327 : Polynomial.coeff recurrence2Scalar4Main 327 = -((5191791652409168130 * 10 ^ 70 + 2180883407228683600931109265685825998696034104800112905798001609416721) * 10 ^ 70 + 7719957409431918230811974734872921324652165580055823386191542065096194)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_328 : Polynomial.coeff recurrence2Scalar4Main 328 = (391866672532194793 * 10 ^ 70 + 7556468485905934245370055782840244645980634279037995869776569569688426) * 10 ^ 70 + 3436204549441663619113975758897244148620978765673419011151285475943856

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_329 : Polynomial.coeff recurrence2Scalar4Main 329 = -((12518275346454514 * 10 ^ 70 + 362261082901951208530493912028486927208497717046878516798496289858049) * 10 ^ 70 + 455130661152440681343425732706267719532901491465687548953313078628252)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_330 : Polynomial.coeff recurrence2Scalar4Main 330 = (175448859240203 * 10 ^ 70 + 4179616810758871379133974612794226713573391832830909254588169936788910) * 10 ^ 70 + 3374997037546132336216271194745666339016193387127838854291173429695276

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Main_coeff_331 : Polynomial.coeff recurrence2Scalar4Main 331 = (2118942344532 * 10 ^ 70 + 4086505362712396858149762652755725608262119058375143947217167804698002) * 10 ^ 70 + 4988857708969314686301494481715154910627760197733587113556916011643586