Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0LeftPart3.Coefficients418To442

Recurrence 4 lookup certificate: Scalar0Left 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.recurrence4Scalar0Left_coeff_418 :

Polynomial.coeff recurrence4Scalar0Left 418 = ((87476451023884187966489968676211491100905204107055 * 10 ^ 70 + 7466026806530210508360492686309426976464117660429980586381610394937311) * 10 ^ 70 + 164747068344296077444472742728676184559074101790979302092462880968704) * 10 ^ 70 + 9074542907395571001903769799953180445343162805530334640858088833223045

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

Polynomial.coeff recurrence4Scalar0Left 419 = -(((52062657662228015405239096182348326819360815127981 * 10 ^ 70 + 9492983279634877908995710095889042176979942956290109329813561839906259) * 10 ^ 70 + 4594432140686731791220982886154868859203809629069702134465125396600017) * 10 ^ 70 + 7681517204709755177191740346244114030340125086693237142380100933502434)

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

Polynomial.coeff recurrence4Scalar0Left 420 = ((24526358911495304362690530631889978241691616247442 * 10 ^ 70 + 6305407651503112716047773843857359171177610472403322085965153464784256) * 10 ^ 70 + 2976356199522112548801597119377677800302036108831324345157659741732391) * 10 ^ 70 + 3356608941199488654032040837619438602841172509424172683059598336080481

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

Polynomial.coeff recurrence4Scalar0Left 421 = -(((10292867318990851416569867434280850689973158858322 * 10 ^ 70 + 5774793727167954781238520940496830154520751704237447853680049985785487) * 10 ^ 70 + 6921451376013253660919884550542476973255235296267357656300433475454906) * 10 ^ 70 + 6451951951460111644681263321976771868067915881357855713564108189109076)

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

Polynomial.coeff recurrence4Scalar0Left 422 = ((4011935456413288747446655769740680673070016957184 * 10 ^ 70 + 8121885992392023179221724313071543451477299120993692634125768242186252) * 10 ^ 70 + 2600413852256236437106103676191313558769315971462248028642819450297954) * 10 ^ 70 + 1123496136423345202344145414993485222732468377536551970120167898574688

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

Polynomial.coeff recurrence4Scalar0Left 423 = -(((1480457794171800503410755568556683265754438334006 * 10 ^ 70 + 3503065689994638795537112559920502151289832232601856002337160421506609) * 10 ^ 70 + 9028772305430468137180083234583938902987545484105416380099957015297991) * 10 ^ 70 + 9316499148110250566103180646012523674737405086612076860249519028660264)

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

Polynomial.coeff recurrence4Scalar0Left 424 = ((522316351655332224728219739981224584331705858296 * 10 ^ 70 + 5569834583213065980955120392033372449230766296660004231858710263996578) * 10 ^ 70 + 5739319118286512560460369198277583889080811228758329374969308947416283) * 10 ^ 70 + 7829819513643423501105965254551207064497074449877423498626237389969398

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

Polynomial.coeff recurrence4Scalar0Left 425 = -(((177096876696559658929637996073126362403873529010 * 10 ^ 70 + 8359928987778996617830216369895904822816912772071731856019323860937921) * 10 ^ 70 + 1581948883635678921313190894176477019846543348295985050025647390774841) * 10 ^ 70 + 2223652396003228729218160699493326900113221410392675341092344201998888)

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

Polynomial.coeff recurrence4Scalar0Left 426 = ((57848899166546141861477923266015007206208917425 * 10 ^ 70 + 9618235820581526998120913215384892462369318091191458115985487419129571) * 10 ^ 70 + 8570247443312934931374341476924359165207962826377561675649503565953047) * 10 ^ 70 + 9163225331883795318234581885195151258061061815092453122697861294398993

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

Polynomial.coeff recurrence4Scalar0Left 427 = -(((18216795910024827244366555530719094049181169480 * 10 ^ 70 + 42995670741800508657371673931739454426467511905841676862440620371936) * 10 ^ 70 + 2503465664473735140134823640078759860144071766665214512957480811467124) * 10 ^ 70 + 1044106440721332702926353334372840680068247525167032944855779167805144)

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

Polynomial.coeff recurrence4Scalar0Left 428 = ((5526195396704808900119319684261535137738332602 * 10 ^ 70 + 9551734164873636562284149867490893356172753427925010890035728231720156) * 10 ^ 70 + 5511504154855260381201438921160708221452724331356524942528748676264216) * 10 ^ 70 + 5989235918446933740926153340611937131532279827432915578924970111551619

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

Polynomial.coeff recurrence4Scalar0Left 429 = -(((1611734269241317660391466307410290456243543739 * 10 ^ 70 + 2732352223862945097102070521838843320579349160144727079264358555086569) * 10 ^ 70 + 2004147633518015529462679936278828934800993609713907649556263799916732) * 10 ^ 70 + 7287579465654637713667458329137221250978739463028077154707063206481536)

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

Polynomial.coeff recurrence4Scalar0Left 430 = ((450406129915567948986481506198456641651549951 * 10 ^ 70 + 4597445001402307511759260750957542576371769189116710917560068537427021) * 10 ^ 70 + 7743035687377124120115197074002325984848705888686300638265065611257929) * 10 ^ 70 + 1298356972741964415685956415710260479172012064353672129208872480393542

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

Polynomial.coeff recurrence4Scalar0Left 431 = -(((119974859671746780706262372073769425481039695 * 10 ^ 70 + 926428044323565655698527079828226295217217459523337029590213863600634) * 10 ^ 70 + 7425230899094063176694601602494331568244110684599385428670088252966396) * 10 ^ 70 + 8033989888119824373984475838892084866549861520498087962540538150022910)

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

Polynomial.coeff recurrence4Scalar0Left 432 = ((30216293284310250774799464201539950154403422 * 10 ^ 70 + 9985518908791690565770939651124960401173070105082753718950087540152692) * 10 ^ 70 + 922352267848252112515602976773532042238541883537163482189476106511133) * 10 ^ 70 + 1778108954296977996010370603987860835596428819955437290698780101798016

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

Polynomial.coeff recurrence4Scalar0Left 433 = -(((7100825092901535680665047880809826247179366 * 10 ^ 70 + 36294975824808011135463328274159034321716309066284144152406333788124) * 10 ^ 70 + 1262736574592597740384437107249364596950508607226933864570354096628060) * 10 ^ 70 + 2936265157775507162331729970583665760850954124500276197628463358433249)

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

Polynomial.coeff recurrence4Scalar0Left 434 = ((1519877335333583080153147442667177690540359 * 10 ^ 70 + 6151287458153113672680514794057105429456809537551213454430106709624800) * 10 ^ 70 + 2364505752445543034911350163938821569463051299768994145802775770421277) * 10 ^ 70 + 8224632743233939708999082611986389623254604436897215172827949580999005

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

Polynomial.coeff recurrence4Scalar0Left 435 = -(((281059011150625158937396554444069614466489 * 10 ^ 70 + 3504228089690854230255508032856303690724397270089191866497990130379791) * 10 ^ 70 + 337359801416608717009949719980561359623352479076953588090440820572647) * 10 ^ 70 + 4274463779490062386910628109807135918498109263929545306308566108757023)

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

Polynomial.coeff recurrence4Scalar0Left 436 = ((38105357847376955897217268041464523080136 * 10 ^ 70 + 5769670612061079169427969797128446416256163221324184480749642177099188) * 10 ^ 70 + 2668802480864249251521072083861439787653179914981719102831922094837314) * 10 ^ 70 + 7845667716409108540722272180272849432765936821215933043875530021286717

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

Polynomial.coeff recurrence4Scalar0Left 437 = -(((265977406446595527394325643828366016927 * 10 ^ 70 + 9234648640661787775455885277639424216679481684277751982989942422054945) * 10 ^ 70 + 5921915449949154097440130462687463165317731136640627477886020599105752) * 10 ^ 70 + 7660594561814384306549348286521714372236372583610743729530597881263648)

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

Polynomial.coeff recurrence4Scalar0Left 438 = -(((2336025255089592652721895630128686030428 * 10 ^ 70 + 3140342321799845454704132842732164446414849894086850168447838756120343) * 10 ^ 70 + 446729440590294050327063723130120010812684121084452638709943145105051) * 10 ^ 70 + 9488790654023998790369216039255424463200824565787311370650378290180957)

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

Polynomial.coeff recurrence4Scalar0Left 439 = ((1145480983380559265051763677996973468154 * 10 ^ 70 + 9063983683324787896951612595499677384549948054827038730562305987051143) * 10 ^ 70 + 49569834947981231231999549712415233928147992306420784197272102832310) * 10 ^ 70 + 907163266315988930670944893765516849692135222134622015527840506559790

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

Polynomial.coeff recurrence4Scalar0Left 440 = -(((402581983546584226858488677325636504073 * 10 ^ 70 + 3319244952304191224298692926356834910269829457424126965387463024640172) * 10 ^ 70 + 5511893799902688970995882711033478447532297693152392802053253234901084) * 10 ^ 70 + 5557251307201275973384339798120109740441117256496084226255697364618479)

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

Polynomial.coeff recurrence4Scalar0Left 441 = ((120911453910668434270122107007771559680 * 10 ^ 70 + 7363815954713060571407195779250851697290918679447747541045898407024398) * 10 ^ 70 + 2947694739936692791061943769570116415010142531184888265547854227906058) * 10 ^ 70 + 6198003997874976394392309871463644210285037400124697079029424780130723

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

Polynomial.coeff recurrence4Scalar0Left 442 = -(((32737138221473539071806120666813541210 * 10 ^ 70 + 7126559903731527521748123756919344483502280547004691655790202734791169) * 10 ^ 70 + 9721360159469603332024780367268294329481609802182244013176139914496810) * 10 ^ 70 + 2700255343567554297937756280412192176536495044423122515566237806802733)