Recurrence 2 lookup certificate: Scalar0Main 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.recurrence2Scalar0Main_coeff_268 : Polynomial.coeff recurrence2Scalar0Main 268 = (6870643032497612720137139403832811975770178008172829323215465401307034 * 10 ^ 70 + 6706064790296676322334506119255120011054819037899481690972383765791338) * 10 ^ 70 + 6517103838095648563918720681927303451246031173926587767324778968202217

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_269 : Polynomial.coeff recurrence2Scalar0Main 269 = -((9071434387300656744863555459653655696272927722143882437128733283644467 * 10 ^ 70 + 4566390950982790959150910688914979475229467051001884813336967788346386) * 10 ^ 70 + 9413967686542535769156146324921471843278347287784950955935136237258951)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_270 : Polynomial.coeff recurrence2Scalar0Main 270 = (7784360680628956793131735795557513654924441229816721887391814400630805 * 10 ^ 70 + 5268934654307807331844305836780320311054168154471951668527415871815336) * 10 ^ 70 + 4579600813031736881418788098054886183616549578017895269647911335039165

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_271 : Polynomial.coeff recurrence2Scalar0Main 271 = -((5604976650371474376379880576376658779658916765133176771140945538209514 * 10 ^ 70 + 5157326342124548097649557506633774239389384888979168754094658954283624) * 10 ^ 70 + 9508580103949126943201127940243209026815598763723748881347266273238519)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_272 : Polynomial.coeff recurrence2Scalar0Main 272 = (3622553259906066889424506418547689926383054846880158178185792901791317 * 10 ^ 70 + 4935702938454318635358596258036864852207871381323911711486594246778583) * 10 ^ 70 + 1362885048673974242397394908522462145387966465540805667358152990636644

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_273 : Polynomial.coeff recurrence2Scalar0Main 273 = -((2159688178277758047526019807965154288505186626792526134058619635622338 * 10 ^ 70 + 3614229480392900016468489946760899471777073454011578069795470251414407) * 10 ^ 70 + 1962469399766151106072618119056196944278037972657565659645307814019206)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_274 : Polynomial.coeff recurrence2Scalar0Main 274 = (1203347489683287888957953205385859777245516979590849855438759541133748 * 10 ^ 70 + 2930439327445779079837250740216779432924713482553709748740647258352692) * 10 ^ 70 + 584764071361317474218539116848847217023402938376904623340612906060559

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_275 : Polynomial.coeff recurrence2Scalar0Main 275 = -((630771405318048481972067602271549906204938050848110075375812482958588 * 10 ^ 70 + 7726122557723912330861936619375460892522404702606934832694033858652700) * 10 ^ 70 + 3431987685775936435595929452901533258284489142227781636445266317077221)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_276 : Polynomial.coeff recurrence2Scalar0Main 276 = (311953769888266717147477942570521185975924848239826865746194948865499 * 10 ^ 70 + 1762462573200235078664770876461525133556949735687650108570779552643111) * 10 ^ 70 + 1493714549259243065005926004948242584829727324542389929953419570321133

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_277 : Polynomial.coeff recurrence2Scalar0Main 277 = -((145604581248372129386812402506973918140659423630959632675351338358781 * 10 ^ 70 + 8321869236028508583966519334523639351630966649298737428696263348397424) * 10 ^ 70 + 154263690775478128850155453268049513605285672601522607651863994875119)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_278 : Polynomial.coeff recurrence2Scalar0Main 278 = (64006734341242971574752935971878136513861911660927771916620240939351 * 10 ^ 70 + 2601481289635096651963133585809712798937660355635190777246587202744583) * 10 ^ 70 + 1215539039081371684597369056486497067194742222944549336704003973959223

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_279 : Polynomial.coeff recurrence2Scalar0Main 279 = -((26369416302474511351991702748880017393273089324099884285134675597891 * 10 ^ 70 + 5266576847865434303203009166034503743315758125070083311410671175047442) * 10 ^ 70 + 3748460545676075023285344160668047515214769275631756721394531844818173)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_280 : Polynomial.coeff recurrence2Scalar0Main 280 = (10086711891390339920152031870044686181364857690164116189594240251699 * 10 ^ 70 + 9348439547787775597771944771993773684971289844759351427091265533137027) * 10 ^ 70 + 6636676847928423854384752174249993309212930257751708205576636145191940

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_281 : Polynomial.coeff recurrence2Scalar0Main 281 = -((3519748484627055095733648929967589934391789700090678298810900178720 * 10 ^ 70 + 8374591445204420182580975743976620398330204720976641570045327032159103) * 10 ^ 70 + 3400011328451092287629430749359060454322039995578450209370907402105662)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_282 : Polynomial.coeff recurrence2Scalar0Main 282 = (1079564085877134136723998565517131319684280730104779409712282076817 * 10 ^ 70 + 1077084818343670440390971375715360080007685233729722709510187259228078) * 10 ^ 70 + 1922115472540555049999126329407864272623513944903739075995024867060113

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_283 : Polynomial.coeff recurrence2Scalar0Main 283 = -((263407349636154058814144562936026495086998114725999877997771901168 * 10 ^ 70 + 1149072376892070061793603850470071270436971347773299322520411234477687) * 10 ^ 70 + 5242974994431394236906202176941885029857578675826304054528588077050354)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_284 : Polynomial.coeff recurrence2Scalar0Main 284 = (30477395520182675843988654389543872746318077054912011341912742984 * 10 ^ 70 + 1702606917801647236581350701935859504071842048182584388778858630478480) * 10 ^ 70 + 5124805223213335591722641509482598875223415338912436396735686850051336

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_285 : Polynomial.coeff recurrence2Scalar0Main 285 = (17301001199843862706153986063753502122977456998342451463416857112 * 10 ^ 70 + 4126015312668081890840233786402741481654441045253520054628773067072119) * 10 ^ 70 + 6334629579689325222475213362517279812425508156878422301254296795901296

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_286 : Polynomial.coeff recurrence2Scalar0Main 286 = -((17178154592780384998740643324907948572015133276940751405438051520 * 10 ^ 70 + 5412385252370748036626740553617352131931467996316932681308930441470996) * 10 ^ 70 + 8600523473073083657017097153493940455012554742969319739475725680001052)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_287 : Polynomial.coeff recurrence2Scalar0Main 287 = (9929703527666010514941471965666723471973824455249250854178818089 * 10 ^ 70 + 4136047052029975235570529817672046740723795502112864061784792651726503) * 10 ^ 70 + 3419010948089986687413684408346488492790178522458445204046773879551327

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_288 : Polynomial.coeff recurrence2Scalar0Main 288 = -((4680148133363474962101062671456464445807973340379341567015428044 * 10 ^ 70 + 8554625344379381999598935315266900413570014327648109146664971503426500) * 10 ^ 70 + 1513188449782906450793551053434492477812565854369094805303017026604018)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_289 : Polynomial.coeff recurrence2Scalar0Main 289 = (1944997934105728537909809995611517141461732941123764436521561704 * 10 ^ 70 + 8109290584156085365518165091725180470705939599582360509159328976823836) * 10 ^ 70 + 2802978947759630986301628026897191717422505666906833224913108444042996

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_290 : Polynomial.coeff recurrence2Scalar0Main 290 = -((733974574886567282986683383747595472709445500679865091926735381 * 10 ^ 70 + 126879366688948754946602258099250948770167765880769801555423434755902) * 10 ^ 70 + 792211523090302576898045521686149682586393223055811334436388494635396)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_291 : Polynomial.coeff recurrence2Scalar0Main 291 = (254671040299420473204591633502579877201283114421646402002725452 * 10 ^ 70 + 6122890686777948410325080221531922817704211097021325593371127781029381) * 10 ^ 70 + 7937438473667589757903249724237760208160825759247477191321015129281722

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_292 : Polynomial.coeff recurrence2Scalar0Main 292 = -((81593028949653090281270595771581161489834691957189004617452734 * 10 ^ 70 + 8740050445443998310654165311758808224510420575647566077172756667400059) * 10 ^ 70 + 257160621962575265983268053606686343995813407673148775753829904323024)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_293 : Polynomial.coeff recurrence2Scalar0Main 293 = (24099865582317701893924815582463473987980984509607503779385974 * 10 ^ 70 + 5733536795676130339256588917408792286925767502264809368440505627557103) * 10 ^ 70 + 9473246119155456136462154001144564252449930395269306869790542449803266

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_294 : Polynomial.coeff recurrence2Scalar0Main 294 = -((6511268119406283555776388124009803224172422892242288006782774 * 10 ^ 70 + 8919900950714033111316609283824498033240389906160445338708808259427533) * 10 ^ 70 + 1026990192570381956923576121523238499828681822819993925465313538502329)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_295 : Polynomial.coeff recurrence2Scalar0Main 295 = (1580654746257439644642123268254651016784049223594536303254188 * 10 ^ 70 + 4192989454369146200606583951279314513867982102526250614094996427133008) * 10 ^ 70 + 1055624806320628061799433154622938099631930335756066664677827394119388

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_296 : Polynomial.coeff recurrence2Scalar0Main 296 = -((331029945764984284118625013025765917109799284645317600102965 * 10 ^ 70 + 8295582293446904385381647051025251403625517882733351735379123766883565) * 10 ^ 70 + 6118085996046015451912764778266475760678537310228505541250039827932613)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_297 : Polynomial.coeff recurrence2Scalar0Main 297 = (53235201465267519004670129727661666239896239344454807186552 * 10 ^ 70 + 6287021945900015696822241981793726499409516379338978969858234796428961) * 10 ^ 70 + 1592637822751981067589362119742361204033176315977283147458297036651851

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_298 : Polynomial.coeff recurrence2Scalar0Main 298 = -((3144252444646942841387116669200278502064066484062521972717 * 10 ^ 70 + 3526201375703888149882438616122259706718182754997096029767353009110811) * 10 ^ 70 + 1855182248129437285389852483669611816824903889245032959012618134293364)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_299 : Polynomial.coeff recurrence2Scalar0Main 299 = -((2135340135035202905643303046878075278796827884143284796881 * 10 ^ 70 + 5377261460185399929594158529296717984894674185566004352452889572906055) * 10 ^ 70 + 7916289920018892599218493157010124363441204972564364556655859752470018)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_300 : Polynomial.coeff recurrence2Scalar0Main 300 = (1251544805318809853035600967582555144135645295272356658026 * 10 ^ 70 + 5279345292206038255658913409593688244508230022670858852506426717540268) * 10 ^ 70 + 4843686839280733773361019758099206362461879900807862424031247222533647

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_301 : Polynomial.coeff recurrence2Scalar0Main 301 = -((460914529475600899294457360596956373883439685344912438788 * 10 ^ 70 + 2549679930242450445341474923372934891440541883075078499285757279463513) * 10 ^ 70 + 5615621487693622521883342272478558072753333554788471683534787547493126)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_302 : Polynomial.coeff recurrence2Scalar0Main 302 = (138698043645754279153869522259711334642013391616701815919 * 10 ^ 70 + 574383965645823312058696380856295591116109781617376417261893444686538) * 10 ^ 70 + 7916638240672625289222870498659028147157567327298197831485913514893727