Recurrence 2 lookup certificate: Scalar2Main 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.recurrence2Scalar2Main_coeff_301 : Polynomial.coeff recurrence2Scalar2Main 301 = -((21170464373738621892723282400915707765604654725164029 * 10 ^ 70 + 2005354607375025425456917305518630485240482709692101557585360032489103) * 10 ^ 70 + 4702688822338671606791305001056985051113400284071334708839983236289638)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_302 : Polynomial.coeff recurrence2Scalar2Main 302 = (2818335266513672689544564166152887145049835559013146 * 10 ^ 70 + 8851955079167670353410343981724639008009727751827563472554543562439305) * 10 ^ 70 + 1706840579806917838185816404055225571502274725558103928006059568010926

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_303 : Polynomial.coeff recurrence2Scalar2Main 303 = -((215211361399415567351107272315201589794950755209094 * 10 ^ 70 + 5468231022731365246238259831858174014361189181265772854079073273678389) * 10 ^ 70 + 7285878249979574234362483347417020387843812891813938018922962558350954)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_304 : Polynomial.coeff recurrence2Scalar2Main 304 = -((25655088010431365572279143252609254877993547523339 * 10 ^ 70 + 4991214762932108103032254120192317444069406465036455732049901020945573) * 10 ^ 70 + 400648382987599903447669309751784866098411133861976379550508652164103)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_305 : Polynomial.coeff recurrence2Scalar2Main 305 = (15928205103947592158422555561978224296959340630963 * 10 ^ 70 + 7627673275098542902887748802610820397293858007146128938800934595181507) * 10 ^ 70 + 2708240677275150731636783017645421963308277289821177729452356014142166

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_306 : Polynomial.coeff recurrence2Scalar2Main 306 = -((4386959081253642078921110532638695914016023872308 * 10 ^ 70 + 217753332414880242100993587655289596256044244120374823897694434253429) * 10 ^ 70 + 5531971709012769387273348949705061796351704254456888681862653796668911)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_307 : Polynomial.coeff recurrence2Scalar2Main 307 = (908386340541312841417722561243374984341361805048 * 10 ^ 70 + 6997534597457597111477425646916549156792054022375932149369079949603527) * 10 ^ 70 + 3431065356562711706644030046578271843926203922449257977122634309717070

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_308 : Polynomial.coeff recurrence2Scalar2Main 308 = -((153727892576582970625211646249494666110700947070 * 10 ^ 70 + 3157952867407460386507911986304199040171756788017394661227110249057387) * 10 ^ 70 + 483636170183262964824708151644094313627477382281470135241732373973273)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_309 : Polynomial.coeff recurrence2Scalar2Main 309 = (21329511856300208254493206760136018560227106608 * 10 ^ 70 + 730987901528999335091067310461525559611321201537574160405723832882486) * 10 ^ 70 + 8451602782769578004067846330579687732620320466505618904751268241749227

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_310 : Polynomial.coeff recurrence2Scalar2Main 310 = -((2273737809544632903579334343738194693119385637 * 10 ^ 70 + 258170183160269288938669151556383570319479619864942123363741459735350) * 10 ^ 70 + 7941333621010097839434944111818590020695005990597597449091659672030240)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_311 : Polynomial.coeff recurrence2Scalar2Main 311 = (134214532129183609346247028275748579473234880 * 10 ^ 70 + 9024370769590953138088075606963309203360134921909464474168343701022030) * 10 ^ 70 + 2162553730386723286667795181185887992749992034386646953055127790633408

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_312 : Polynomial.coeff recurrence2Scalar2Main 312 = (12493424611427153331723093530042274950986344 * 10 ^ 70 + 2725885380839457228711446693456085468073345574437023874542682530203666) * 10 ^ 70 + 1915751790479403540664216535013896867132779670421623625448440027984032

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_313 : Polynomial.coeff recurrence2Scalar2Main 313 = -((5623120651188670557216490603122332544579835 * 10 ^ 70 + 5009011802452248627798316418850390195461864112543017447373758251070684) * 10 ^ 70 + 5892977886891049393813272068943568446527707148331420432777078992408624)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_314 : Polynomial.coeff recurrence2Scalar2Main 314 = (1094627725689114679939767731310066714665936 * 10 ^ 70 + 8613430256961959816411554316216628310232233787158288573508804359368898) * 10 ^ 70 + 6876170679520880940546423002959395085770768215571139520602774105655519

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_315 : Polynomial.coeff recurrence2Scalar2Main 315 = -((152322329276388894703369238461401004621429 * 10 ^ 70 + 2071727273759022031729247174845498340554286329096792651829175919794879) * 10 ^ 70 + 2072902017167960799491923996379719192616435017194247746103673328365149)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_316 : Polynomial.coeff recurrence2Scalar2Main 316 = (15819122470015665910992181377801554309292 * 10 ^ 70 + 6879864347272926119564600229840575905641830316120438654097142405459297) * 10 ^ 70 + 602524327239836364990104917267582970435763648925864573508362915964892

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_317 : Polynomial.coeff recurrence2Scalar2Main 317 = -((1062186299827485473260143374495715951985 * 10 ^ 70 + 8190507185592081405625976989047999636488739421269874205430186847035961) * 10 ^ 70 + 7735853662510747333926469955350307212687431782032580374301082840224305)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_318 : Polynomial.coeff recurrence2Scalar2Main 318 = -((3277274167399156481628990860054198686 * 10 ^ 70 + 8399683847141329859111034426049221386923083304450282620486716418075408) * 10 ^ 70 + 9270479854303926060135031995360199710292642127739598048935096308036830)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_319 : Polynomial.coeff recurrence2Scalar2Main 319 = (14052810434814592773488023583126804356 * 10 ^ 70 + 6447120347516446576348628795275991725501857932312943297203123445754813) * 10 ^ 70 + 3833343933953923181915030688551532504725252350260330989643622014350673

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_320 : Polynomial.coeff recurrence2Scalar2Main 320 = -((2542839945280669067068779188464862129 * 10 ^ 70 + 6857849923422792389498570921546401530915180192915882748837986182681112) * 10 ^ 70 + 4326370489746372772049067422101734539919500642544068242493471145099284)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_321 : Polynomial.coeff recurrence2Scalar2Main 321 = (295948849442373561357637745468246236 * 10 ^ 70 + 6579984425521036463205478091040163134742478981212887897483290523553486) * 10 ^ 70 + 263116087574954176364395147421694387111691756129375970903971006585724

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_322 : Polynomial.coeff recurrence2Scalar2Main 322 = -((24710175853541087079412258605580274 * 10 ^ 70 + 721931195676762484002714807196424711226250580945101510293940982412232) * 10 ^ 70 + 1827977440969843812306317149317808464663648373121335104737272936925142)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_323 : Polynomial.coeff recurrence2Scalar2Main 323 = (1318067843596303020768019824171823 * 10 ^ 70 + 4955282190335643988263266404502789172659911119371340205010922487843356) * 10 ^ 70 + 3342963927825168248765157518894225136859643166183354123360205880495272

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_324 : Polynomial.coeff recurrence2Scalar2Main 324 = -((3440268919530050578897182983972 * 10 ^ 70 + 7594123071135407788648519926287338364974265920186339717689481945214392) * 10 ^ 70 + 9009862114180293073463305944877940585635150377962733642110885957196739)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_325 : Polynomial.coeff recurrence2Scalar2Main 325 = -((8612396978175425338299635825288 * 10 ^ 70 + 7952397604936050040695237547512556002453747523208064048495573268117365) * 10 ^ 70 + 5517516950473533206185401284673676909104151330845881785550274725559995)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_326 : Polynomial.coeff recurrence2Scalar2Main 326 = (1137800376346997074717370633265 * 10 ^ 70 + 6270307366110326573780707870135769021608089403559152068625159929994570) * 10 ^ 70 + 1109204244692620464787811483283567230180240331324369300644546239875809

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_327 : Polynomial.coeff recurrence2Scalar2Main 327 = -((91113373652381188597690792524 * 10 ^ 70 + 1231599359758260903058147361686587757964822111519295372480622311096432) * 10 ^ 70 + 3412942152055605559285595920246158234756362922431446171562884353253148)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_328 : Polynomial.coeff recurrence2Scalar2Main 328 = (4854101435780678867137455408 * 10 ^ 70 + 6958051198896089101005677151646466941692374100146289079919406125039712) * 10 ^ 70 + 1915634390641031943100230466982689542846080894929449585641126981106982

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_329 : Polynomial.coeff recurrence2Scalar2Main 329 = -((129484358716314561343049955 * 10 ^ 70 + 5248290170096731013173709481002911288764758523226392088073889950400273) * 10 ^ 70 + 5617462862894627022773460538635769623325604119233950363490147015244871)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_330 : Polynomial.coeff recurrence2Scalar2Main 330 = -((4834140668658228414622796 * 10 ^ 70 + 2381709052288710624763333875077545610257970186017344995258530784940248) * 10 ^ 70 + 8809803769509955877999670913271053538038894234458522808266203367822030)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_331 : Polynomial.coeff recurrence2Scalar2Main 331 = (812470723025451525638503 * 10 ^ 70 + 714266932153122161568777010869412299690523606483276697276677210589086) * 10 ^ 70 + 5615215207595992939558384408823771199612657979247605745420280810932009

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_332 : Polynomial.coeff recurrence2Scalar2Main 332 = -((51781133944453125770478 * 10 ^ 70 + 2018884291292624209460456316632194113853888774350251383030210678397435) * 10 ^ 70 + 8140836888662381089748873835881246055735220846084241528215786095279184)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_333 : Polynomial.coeff recurrence2Scalar2Main 333 = (1933271236309310659642 * 10 ^ 70 + 4358302118899262565506374346696887937381918037156248304679024788282996) * 10 ^ 70 + 5590257062998279798213994455944998277593251919053449117227180812887720

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_334 : Polynomial.coeff recurrence2Scalar2Main 334 = -((29788584645904823362 * 10 ^ 70 + 5921042944680545484185039213940110634970834429435250646879398366463319) * 10 ^ 70 + 1697767399389660911661252438723971863870519912154999836886104977962603)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_335 : Polynomial.coeff recurrence2Scalar2Main 335 = -((1216519198774344766 * 10 ^ 70 + 6646633470664584609493074557394472002154989818695760980301716601851023) * 10 ^ 70 + 6108598999330270694330817342780544502405429634534461022920093523208390)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_336 : Polynomial.coeff recurrence2Scalar2Main 336 = (98711194334625607 * 10 ^ 70 + 239722173047649738846032839511052751195331784676158871118841948302414) * 10 ^ 70 + 5043221868932920126344327952838464598915450543025680109667129642048246

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_337 : Polynomial.coeff recurrence2Scalar2Main 337 = -((3168224069642583 * 10 ^ 70 + 1654390563671621239163998895305793906581644684972735033235382671948268) * 10 ^ 70 + 6692646703441075721880617125409359004249885537522571617712933216517669)