Recurrence 4 lookup certificate: Scalar2Second 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.recurrence4Scalar2Second_coeff_424 :
Polynomial.coeff recurrence4Scalar2Second 424 = ((164780662462622325359469039247215453957851980 * 10 ^ 70 + 6993993168091601198745062779730758675688019771000898123282393615767152) * 10 ^ 70 + 119010887467248644771306923763239303740723273759982486102277178930466) * 10 ^ 70 + 8234818638546556832266596726315512813124737379839910846189868459780473
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_425 :
Polynomial.coeff recurrence4Scalar2Second 425 = -(((45091874752896831696565080032115461851343095 * 10 ^ 70 + 5506243649281618125254095443082391177486819458253197829926171836930714) * 10 ^ 70 + 6055786000999109668603244157696424678342802275822942972069535453182003) * 10 ^ 70 + 1370860580581611059408415071658233768921717605151288837349584352169271)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_426 :
Polynomial.coeff recurrence4Scalar2Second 426 = ((11661151472686361324143124985016066097628148 * 10 ^ 70 + 8517015912903218637717649197978162574483559538336068904641412016044751) * 10 ^ 70 + 2517583747271856718175680986767939352192931650217099088090755227197048) * 10 ^ 70 + 5879067342013708205768061950002066363426663517931928068942321692847623
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_427 :
Polynomial.coeff recurrence4Scalar2Second 427 = -(((2815398486048892420997387102843053534993141 * 10 ^ 70 + 5864627804467813194235553135639605987789837900777301201683167722918938) * 10 ^ 70 + 3964481960492609983508624280440562575043175497319595426368431378754361) * 10 ^ 70 + 8924850015202088406960747784872960110533061482892630196951683867116354)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_428 :
Polynomial.coeff recurrence4Scalar2Second 428 = ((620991241758961415419300612100046813607585 * 10 ^ 70 + 2923000125394812791595758966646478887559169374709211049650203569308821) * 10 ^ 70 + 6356825140521699829236566370890511421134029433316111344540817824844737) * 10 ^ 70 + 8906754151266977976583762078366671437779251452453538307608658916347412
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_429 :
Polynomial.coeff recurrence4Scalar2Second 429 = -(((119546659637121521459535275379549356629284 * 10 ^ 70 + 8340510300830570786608678905964087448818573174849157189497948855799985) * 10 ^ 70 + 9991162850187627185060573850778356045161814905600693807327071270086670) * 10 ^ 70 + 8773645478811146708720774200053301049842045978034491041726774427442553)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_430 :
Polynomial.coeff recurrence4Scalar2Second 430 = ((17613991774016421564791489360659172105406 * 10 ^ 70 + 7592006031937224459448878574567959180262074590748371667547800967450513) * 10 ^ 70 + 7368311948765229555536726401247456072048369284796315589195465243331638) * 10 ^ 70 + 4506916667665925458485047556731623548367768171906697996926024296868392
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_431 :
Polynomial.coeff recurrence4Scalar2Second 431 = -(((736659179960596210971055273221154910995 * 10 ^ 70 + 8405457577191949975785200257649636748762255149893480971501491764717193) * 10 ^ 70 + 4810461010592422297318075028453440455545804455696975872572975140030386) * 10 ^ 70 + 7625448831141801475870016533059632336443028386561242857432045554508429)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_432 :
Polynomial.coeff recurrence4Scalar2Second 432 = -(((793752699972652138849312554735857148663 * 10 ^ 70 + 8239191679094930629357594476005628229952986025457661181013222126494417) * 10 ^ 70 + 917723449936951136133682229748840289547650213872354809976400157688377) * 10 ^ 70 + 9497113500757767488991682639382460180778397244678174238933030348302498)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_433 :
Polynomial.coeff recurrence4Scalar2Second 433 = ((432069074281742271879655632309666337512 * 10 ^ 70 + 9897868961801241256971758150669827749437701017363818131451203599832081) * 10 ^ 70 + 475195361686466203480004535365452737440599942718831278413338656186008) * 10 ^ 70 + 7014017428966335463791093958635784663630480086430878469923997121109464
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_434 :
Polynomial.coeff recurrence4Scalar2Second 434 = -(((157269419995314688245163554790850804194 * 10 ^ 70 + 5978861148734566780107243987527739343945312174208525787277896222806190) * 10 ^ 70 + 4255725849057223555165712509291840345350770379832335331720593740917857) * 10 ^ 70 + 437407965179544356453187287950608461124285418305705847337449531422468)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_435 :
Polynomial.coeff recurrence4Scalar2Second 435 = ((48045114306676685971388444993852890838 * 10 ^ 70 + 5348943463908666922394316160663105726757399120329342904299199232768617) * 10 ^ 70 + 3373915204981488142031699533160285835324605257797959260720441013646039) * 10 ^ 70 + 7622626588515093892830201110291475586981152259721980035486567937187234
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_436 :
Polynomial.coeff recurrence4Scalar2Second 436 = -(((13110163102480108470102194290624099876 * 10 ^ 70 + 6530334581133266280905265841499385945872384248132658688966869891036156) * 10 ^ 70 + 4883353507748966475121865969792400453845682564329831035589756131770337) * 10 ^ 70 + 3273550048760452641164607862057403184267956399443009915115562264566203)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_437 :
Polynomial.coeff recurrence4Scalar2Second 437 = ((3276595342382490564917959221431736350 * 10 ^ 70 + 270922953434187614560274914769352693680711186087642323016725636492882) * 10 ^ 70 + 3348473445090886274208026457243220302989497479114889073057187881159806) * 10 ^ 70 + 6787994257826034028769677426123830086825551779425382295259167852059979
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_438 :
Polynomial.coeff recurrence4Scalar2Second 438 = -(((758805710912035408401982118382466577 * 10 ^ 70 + 742871833230143851908015715567838260879614249532280391842108825343196) * 10 ^ 70 + 5138046388921479206264536764111420361253138173256998420857356855536065) * 10 ^ 70 + 7390794053573933225610069627933086211875607385205608274723438242754443)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_439 :
Polynomial.coeff recurrence4Scalar2Second 439 = ((163673537480066441041870062860359513 * 10 ^ 70 + 9316582351691554244125156356845915073933303710301886718946039918564984) * 10 ^ 70 + 1254446479811114139813892099460676909142680573242091056060377843290819) * 10 ^ 70 + 6159858072120732924297296161690097185634607710654018119116809305855942
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_440 :
Polynomial.coeff recurrence4Scalar2Second 440 = -(((32926429242139503608579280162845895 * 10 ^ 70 + 6185737585976596141269239239420621505288516517831243606420065727281216) * 10 ^ 70 + 7176761645424310299215159786645174576234873270616821840107145854151331) * 10 ^ 70 + 2050869138564947039278922817822119249011296903343753610632155254199234)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_441 :
Polynomial.coeff recurrence4Scalar2Second 441 = ((6167667844965404942067959332992127 * 10 ^ 70 + 1036629597624106339108317393936549289880894172085472520735036252567079) * 10 ^ 70 + 6819253012154449897885079785785710732154409311123918809485742594116738) * 10 ^ 70 + 5960989432368620863904942291725923591708549698453699981843385737995593
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_442 :
Polynomial.coeff recurrence4Scalar2Second 442 = -(((1070726584205785044738918285234268 * 10 ^ 70 + 9566740882179156074471474235253017559826996635593151330336840512824853) * 10 ^ 70 + 7359870918888888086666103797443017540700860311832927009167908444467089) * 10 ^ 70 + 3535476901498395914280213961336283607734260839465925647853767138963367)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_443 :
Polynomial.coeff recurrence4Scalar2Second 443 = ((170765371026368260757174483901687 * 10 ^ 70 + 6277590127268297728130993880076773023211580875544172951364938627592862) * 10 ^ 70 + 7727643971677004602595715885765760026745860050054020019097796517072066) * 10 ^ 70 + 9783078990677835504537998483905427077525162132568124243347491430795401
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_444 :
Polynomial.coeff recurrence4Scalar2Second 444 = -(((24626309954683550120593863822881 * 10 ^ 70 + 3519161510661082259691506989512776790661498390622022033555395958829216) * 10 ^ 70 + 5728112861651240801987696108203551761730283918102900628207066025989403) * 10 ^ 70 + 3215642569582519772720162272539774870281985019878501523958585155137874)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_445 :
Polynomial.coeff recurrence4Scalar2Second 445 = ((3113368322824740457758185963490 * 10 ^ 70 + 7388962727859133498085588895518725765539506235991213064196750039691347) * 10 ^ 70 + 4461770126352647277804038352329210200997627978860851883422018338283711) * 10 ^ 70 + 8089808359004994773649919904509265655770730414880474553536184136405479
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_446 :
Polynomial.coeff recurrence4Scalar2Second 446 = -(((320558172272480639370358133474 * 10 ^ 70 + 4327671519813289745625890646010792027478088314734710295707847329794169) * 10 ^ 70 + 5351960922296548739866092506097838383464101882707374187824816740968145) * 10 ^ 70 + 152793404221969409614841836821402476311274723700008624428465352411524)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_447 :
Polynomial.coeff recurrence4Scalar2Second 447 = ((20351041710268114659293878274 * 10 ^ 70 + 6167025714354071385230514546713990454448702456671928919251355264664556) * 10 ^ 70 + 2457995219704911745638239012182424574896275621670866941426704117845449) * 10 ^ 70 + 7390852130316816938908301285537536464620292834771840364606052619876713
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_448 :
Polynomial.coeff recurrence4Scalar2Second 448 = ((1231373220293710108350461824 * 10 ^ 70 + 6953375222458084894599165201827464434666928992370991564119849869301902) * 10 ^ 70 + 1776061720377478655734952189959451485389205297104196349091512825871053) * 10 ^ 70 + 6272458610600658096280846591692817603796560660371330746758227868058382
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_449 :
Polynomial.coeff recurrence4Scalar2Second 449 = -(((722419293867099086142045695 * 10 ^ 70 + 8374216141205462041942905541548376359458796901003096123674880344532703) * 10 ^ 70 + 2710306294568467991784753848438812775005807481835900080436968850448234) * 10 ^ 70 + 7933942703113751334239989292108242213021908820440826333141643150409738)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar2Second_coeff_450 :
Polynomial.coeff recurrence4Scalar2Second 450 = ((158344584194332632583826392 * 10 ^ 70 + 1080974622447210442725747545438895670828225402383643312796191054741149) * 10 ^ 70 + 7411609808754016936128479160569148504424935151234412907830555275253930) * 10 ^ 70 + 1379727851671197507969849406774010381262122845195896004265143456733837