Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1SecondPart2.Coefficients355To382

Recurrence 4 lookup certificate: Scalar1Second 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.recurrence4Scalar1Second_coeff_355 :

Polynomial.coeff recurrence4Scalar1Second 355 = (((516624 * 10 ^ 70 + 9155533746037275718399554893075158133579039442336310021235568087161434) * 10 ^ 70 + 4452671729956879610410437625941548583391441933052323725101608778936450) * 10 ^ 70 + 3133324295909999664669335274521757636630347243913750116147991947491421) * 10 ^ 70 + 4685540026032915995056517350741324515600887037447072767663323415471727

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_356 :

Polynomial.coeff recurrence4Scalar1Second 356 = -((((159891 * 10 ^ 70 + 4989757642575665820462590664351205422497760627926398067763253175829203) * 10 ^ 70 + 7764284959187570149990515052816695603009568681250680146716403337565200) * 10 ^ 70 + 9924353175982807539990865185018480732962906744002642651355695855642760) * 10 ^ 70 + 3654123309266562592418229019610156424171333125942627167611845513909955)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_357 :

Polynomial.coeff recurrence4Scalar1Second 357 = (((29740 * 10 ^ 70 + 6464312404568459510017671015328373336919726901769504371411678750448739) * 10 ^ 70 + 640640952270998559296183728836788254155989543352447150251504897583653) * 10 ^ 70 + 5364701752759133608668207478287469397548746117616892834351289290246430) * 10 ^ 70 + 6668018460921442885070179022923165156026725893408753050180219480402916

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_358 :

Polynomial.coeff recurrence4Scalar1Second 358 = (((7139 * 10 ^ 70 + 1271717050645764515211493995896017904340071920041515055176082529163379) * 10 ^ 70 + 3903898402662103648633942228905852029485725612270448445178118602033685) * 10 ^ 70 + 9683429632128117285633499822682957919586088521224856920592229839298321) * 10 ^ 70 + 6478580791674359422632544569809766824396761900743503038644388205814413

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_359 :

Polynomial.coeff recurrence4Scalar1Second 359 = -((((12057 * 10 ^ 70 + 4525084507176267044867584806187306636927523769107791400708082591490820) * 10 ^ 70 + 7053917972954662747716529161442949858772422505855351041159578028579615) * 10 ^ 70 + 3527519570674090431338447066792061088314752574048407918134934729191322) * 10 ^ 70 + 206524963913474234568744194291698915824265475677638492004945827583658)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_360 :

Polynomial.coeff recurrence4Scalar1Second 360 = (((8849 * 10 ^ 70 + 9613691643608132588501886726356881639823169692938133081413832247315683) * 10 ^ 70 + 4845749221462237696505174427125688170263838039461348870065747065067563) * 10 ^ 70 + 4630151523106239085992840636100576232715031339535056224329715460843426) * 10 ^ 70 + 9232952870097982372172238869007582139933186326510303894790537228435296

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_361 :

Polynomial.coeff recurrence4Scalar1Second 361 = -((((5155 * 10 ^ 70 + 9436699903447168423987863187671277976355708324171756452793647432390621) * 10 ^ 70 + 8274954470379568089237317494426490444777834800535652266385700467310831) * 10 ^ 70 + 7720226407379515727294533637311017371755551344500112387080449531242465) * 10 ^ 70 + 5715455079206152461947163132275396737170469653898029330112132174912686)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_362 :

Polynomial.coeff recurrence4Scalar1Second 362 = (((2655 * 10 ^ 70 + 594249025792162452622344031252007511640318942869403742435686676400881) * 10 ^ 70 + 8490768023162478078293499119339200379833755182602129388096681211918075) * 10 ^ 70 + 2467100454809195671673149467244049838670504147817104136741281917273503) * 10 ^ 70 + 9677476549855533402436962459509863268787043997944722234287734239099246

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_363 :

Polynomial.coeff recurrence4Scalar1Second 363 = -((((1256 * 10 ^ 70 + 4194186958647408789426341907657607973627718782798274943373598121378557) * 10 ^ 70 + 1812348308812499559402543712657600109650206100858632980654667695489106) * 10 ^ 70 + 7574718272170073634431260491564369983553315022026167888435349049123136) * 10 ^ 70 + 9694629680915400228599523112088938047300731145568491499786055438097541)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_364 :

Polynomial.coeff recurrence4Scalar1Second 364 = (((556 * 10 ^ 70 + 543644527874415269170322063093725164740231050004246697620968561095600) * 10 ^ 70 + 1888396274153950565669913973290433184215904414742117737353705862004937) * 10 ^ 70 + 9138773063448824980906894564873229345259672517567587889978388965838808) * 10 ^ 70 + 4361993538900823249275213131179637837456894477093054458700467467078950

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_365 :

Polynomial.coeff recurrence4Scalar1Second 365 = -((((232 * 10 ^ 70 + 349737851736920570137680972736201659515707141371943245260860216301952) * 10 ^ 70 + 2230243799326685802127261179359771952079947081713993300172717626351230) * 10 ^ 70 + 6328794591236587540081580127476437830686231043536538024966600728046769) * 10 ^ 70 + 2091532147940099194103747118009062597197185568409573852898700332445480)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_366 :

Polynomial.coeff recurrence4Scalar1Second 366 = (((91 * 10 ^ 70 + 5300659312116488335686017565730898141473410230385744586022712182145754) * 10 ^ 70 + 6209598653423026808916848474044099036449836614121635130611556170921553) * 10 ^ 70 + 2829240269832150809523049661360861805265738019647496034138820414463323) * 10 ^ 70 + 9398367000669067995979181001554542873794341603870512838124350062925384

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_367 :

Polynomial.coeff recurrence4Scalar1Second 367 = -((((34 * 10 ^ 70 + 643297018456123372011695133445926974469179003328222107252891223268262) * 10 ^ 70 + 9101937168848926659503926923043194021367277038812951699329375053068827) * 10 ^ 70 + 9611441288970658160282701076958935970300688847136201374771970742410676) * 10 ^ 70 + 646210964528337134116881963515865756483414593891451976175692529242261)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_368 :

Polynomial.coeff recurrence4Scalar1Second 368 = (((11 * 10 ^ 70 + 8735410801029890450084147373367270127267743735186475534422931675456294) * 10 ^ 70 + 6368262208535443028041841181992388276479794064452049526927381125805661) * 10 ^ 70 + 8350889789757631813889933459307929824110257448956675012497717670055386) * 10 ^ 70 + 3090020666449654347537705070228341279388036409738019354321167620572229

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_369 :

Polynomial.coeff recurrence4Scalar1Second 369 = -((((3 * 10 ^ 70 + 8135791832568568251882013930792865164559344901839652313493373922050634) * 10 ^ 70 + 8921347901410939507891191447763511686637827954845999453168886942648078) * 10 ^ 70 + 5383744522024492017803446925464768870678037784118588984108035816232693) * 10 ^ 70 + 6412639027633982445977512592179662517249678137769746179562742285460268)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_370 :

Polynomial.coeff recurrence4Scalar1Second 370 = (((1 * 10 ^ 70 + 883378619583598393144176037189326743310443590431326211035419606506077) * 10 ^ 70 + 5349299100886933847021881661935794157020598159063056242745154041968972) * 10 ^ 70 + 7120740404820021219025227812506413091630713766311256214854249189018375) * 10 ^ 70 + 9158205370105492305869532404565204277269768161087213029503426817589397

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_371 :

Polynomial.coeff recurrence4Scalar1Second 371 = -(((2496898247036375192303984922275487301821368831778476618377730658502274 * 10 ^ 70 + 1997762733767119303800593248072946011957001061873177846048464660317215) * 10 ^ 70 + 7510922432008750212789315810085286470157262034430095389596154000686182) * 10 ^ 70 + 41709869953764184446398841447935929217444683090750770602891809252016)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_372 :

Polynomial.coeff recurrence4Scalar1Second 372 = ((271195554955399855903143585930520871896629991117224788419080405769387 * 10 ^ 70 + 2258819514470835007083940849936662544678481664397561014952326936858889) * 10 ^ 70 + 5843704732153114897873910456569046847413180371486772917361135607895646) * 10 ^ 70 + 4375325843873028145567781967576994477035283920943744635771071774681100

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_373 :

Polynomial.coeff recurrence4Scalar1Second 373 = ((155243376242138007743502402813369603809405302637422835888749923721696 * 10 ^ 70 + 4535130659415761706625157667014370651950298147645272485734488810501933) * 10 ^ 70 + 3967039106040970718712083183372126759327611399282954304929847544216228) * 10 ^ 70 + 5470786349308036517900640771030442397642289589864003403993229827754464

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_374 :

Polynomial.coeff recurrence4Scalar1Second 374 = -(((149778672661499806735611808176348574172392360210217473456936714215004 * 10 ^ 70 + 1671174358680316558555050822138993708453056562166457216800931345646652) * 10 ^ 70 + 1459735746510717987376177512028302177085550658734847400935214082934136) * 10 ^ 70 + 414651827985511303075910334330437443085229067098465005483636871044601)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_375 :

Polynomial.coeff recurrence4Scalar1Second 375 = ((85995902457846716077693475686658398271956549645776148204526859921098 * 10 ^ 70 + 6515896994335735193301364953524167252745382633041760215464414216874148) * 10 ^ 70 + 8532368076821147065512532109807331648752485287550717342608868863679061) * 10 ^ 70 + 9813229515716151963763759457654133989074414141862626246312058618910447

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_376 :

Polynomial.coeff recurrence4Scalar1Second 376 = -(((40892128419825681008509688176414286340308327615339623688961650751046 * 10 ^ 70 + 2327216217004501881360760763408603922339045993035291390959503665388168) * 10 ^ 70 + 650023848396163098819316616329396551212964392838165525344271025069054) * 10 ^ 70 + 2215462150289389864470658923491873022590671720139267726866515926582641)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_377 :

Polynomial.coeff recurrence4Scalar1Second 377 = ((17398859442015155497107044273474371914039783798455435003236597334893 * 10 ^ 70 + 9319791734215406317117673660306527662603898191235010388769036421942847) * 10 ^ 70 + 9540706512396171291579145564771951194186050266870853633418688659899518) * 10 ^ 70 + 5778110906673061894379824565878996159908997942680231525998169399997595

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_378 :

Polynomial.coeff recurrence4Scalar1Second 378 = -(((6817594412262318650560289996018346846896753360225698591587574886549 * 10 ^ 70 + 340768301060780499352491464045630338564651138365086833639676779583033) * 10 ^ 70 + 7507102959517449209081934800815968741177955883388879748977194813753096) * 10 ^ 70 + 8261111309919377220473783689696486055280661747168432739607256299985266)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_379 :

Polynomial.coeff recurrence4Scalar1Second 379 = ((2488812741878293392346288290552315878963525546586970934274470681452 * 10 ^ 70 + 6047688947140206997629274198938512466021001936218651976624192727113935) * 10 ^ 70 + 8371470499848274901515717105152732225078039307106520857308932956735801) * 10 ^ 70 + 2113187596149538142528848228896182125305093132095187834060378296580649

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_380 :

Polynomial.coeff recurrence4Scalar1Second 380 = -(((848495656953926538025589810562134411157799312299593748391041974907 * 10 ^ 70 + 81971276417629994404212082707628531819646204685900313241178066100208) * 10 ^ 70 + 4531111520725130401296508526008209502309308397780857199870815453661473) * 10 ^ 70 + 178726231274816389621864011881770603794008318262650568132598676446688)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_381 :

Polynomial.coeff recurrence4Scalar1Second 381 = ((268736159083725851040039925299793505077279180231752802230014933742 * 10 ^ 70 + 3319383351854366574099600979567273303689140924622925411794310026905510) * 10 ^ 70 + 2569994727389349999496309918313094765549726021377915946322649638016214) * 10 ^ 70 + 4145264322499070436580640414316164653424454438660233327153868563468071

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_382 :

Polynomial.coeff recurrence4Scalar1Second 382 = -(((77834989043484279630500503874620088847621235238428890266047464055 * 10 ^ 70 + 7747194725252433054601980415109704056901395911248689133335087068716338) * 10 ^ 70 + 247984145566361680069701230139532933329018826842048438512634730238802) * 10 ^ 70 + 1676177300902521457710665406856624555744297816151390562289137564765272)