Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0ExceptionalPart3.Coefficients407To430

Recurrence 4 lookup certificate: Scalar0Exceptional 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.recurrence4Scalar0Exceptional_coeff_407 :

Polynomial.coeff recurrence4Scalar0Exceptional 407 = -(((41429665483284133119883178900372317275373715484395926429 * 10 ^ 70 + 9421479310685325998446173566687875027823583093233371806417193396048930) * 10 ^ 70 + 6934077770353185629751081477415028792055451747964782068450497335477102) * 10 ^ 70 + 9757437858560708385517113653265451742806394080770797456069760687243650)

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

Polynomial.coeff recurrence4Scalar0Exceptional 408 = ((5570818648312750018458961660687588901035895037739170012 * 10 ^ 70 + 5126991629709365386932491809791559440653447064814159802912656484512703) * 10 ^ 70 + 6492571794757620805482613045628208156930938989060866939403659617163574) * 10 ^ 70 + 8046489731820993393229120583758340065509710452198451162381950165042668

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

Polynomial.coeff recurrence4Scalar0Exceptional 409 = ((656198430228002373569556812568487875463660042793028543 * 10 ^ 70 + 6255650352572697402019466843092386174165199272240953229261836854365522) * 10 ^ 70 + 8696847175709958525900278294900806344211099699352932460113053276835787) * 10 ^ 70 + 9160221672656448443219589221561580634061062563506672432879750745403801

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

Polynomial.coeff recurrence4Scalar0Exceptional 410 = -(((920412901916014344735514882385318097971281866304218893 * 10 ^ 70 + 6831532111748675930033065461814484310289495392364135668691152455473770) * 10 ^ 70 + 8343576772979484962407494896401077468230752029214903084871907991764688) * 10 ^ 70 + 9644085069745485369089688349220118824971013304171522501491250291526415)

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

Polynomial.coeff recurrence4Scalar0Exceptional 411 = ((481626565510826243437136507015861400876143291265071720 * 10 ^ 70 + 346708003136313074087808423272625374780688478561525722826885881789293) * 10 ^ 70 + 7819956941910602410185351878123275551957630321702237653097954840263161) * 10 ^ 70 + 2227673681588745378709213631153257108714082701176172047870386415002801

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

Polynomial.coeff recurrence4Scalar0Exceptional 412 = -(((196844067355451967594237813437211097047049094708952165 * 10 ^ 70 + 3800467965765641857007129482758913520294823142562750007047836232875069) * 10 ^ 70 + 2331402134834873408682893193446367843013800571948503904642629371482062) * 10 ^ 70 + 2009087110570157638538693495744529438797896444097621363774401597436931)

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

Polynomial.coeff recurrence4Scalar0Exceptional 413 = ((70416065270452779031360162147099246613669611745336996 * 10 ^ 70 + 4806655454352131369748185511681581809346994395308530948192421162630843) * 10 ^ 70 + 4403409843523730429261675259518874961047255718734802290403224334271522) * 10 ^ 70 + 1602751773831387682423437367406420158039946579058811153106519086904875

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

Polynomial.coeff recurrence4Scalar0Exceptional 414 = -(((22882663212835547539760969905907958477731880753765399 * 10 ^ 70 + 7731937788477214060073565930835669283669005803303311440411150643415437) * 10 ^ 70 + 9623058175666250892307896304744170376258906648565659152081628835946356) * 10 ^ 70 + 2992925851290132766159593812739012569226313369377240209540503800346272)

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

Polynomial.coeff recurrence4Scalar0Exceptional 415 = ((6842969743337162984347365024704063438395062133598285 * 10 ^ 70 + 3555099811925814528899414480806368937321970126843105042564536700264320) * 10 ^ 70 + 2157742881314618357293187388873322300979507552821514253669909685402078) * 10 ^ 70 + 2297161876252166866620324229978404290542322486716278843148540632068923

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

Polynomial.coeff recurrence4Scalar0Exceptional 416 = -(((1883310982253723322013751752735123087257282253893691 * 10 ^ 70 + 6429824986455187860855692567247654821766521874255010214494387599110549) * 10 ^ 70 + 2856774598220067989281715131021966860527507146751789176010731176393312) * 10 ^ 70 + 1181825394646277073236996012884043868847142728256098352720946717862751)

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

Polynomial.coeff recurrence4Scalar0Exceptional 417 = ((471274012538713354102135600094835885829092677639626 * 10 ^ 70 + 7436481551164849540198118226563912557426405828683602698367284859835158) * 10 ^ 70 + 3283791375774518870576371971253229466188124070868925409521587342502543) * 10 ^ 70 + 2499827325859187781990262389105704434610653793143246305672020672733578

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

Polynomial.coeff recurrence4Scalar0Exceptional 418 = -(((103734961226911323312116733402754124705453469536777 * 10 ^ 70 + 6108700789822735320626836629391117084035052541625196636171860518606268) * 10 ^ 70 + 7291085881022976911002055202551750438937725688839872213773660039707939) * 10 ^ 70 + 8346739798745264951344390991498744890696161586546014587349337761339184)

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

Polynomial.coeff recurrence4Scalar0Exceptional 419 = ((18301088759530512064729082291467574535748184723812 * 10 ^ 70 + 9923047804580879732717707982531658564793659965189790577212376095835568) * 10 ^ 70 + 5198269222561570333666738270366289194835122860408949297222459850989312) * 10 ^ 70 + 978614847517419472592950227277679600854716864241755856348736553738965

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

Polynomial.coeff recurrence4Scalar0Exceptional 420 = -(((1637354131430140398887350379809136991373190747273 * 10 ^ 70 + 8762705199013912656953826272267511316953270315932375412937698891732662) * 10 ^ 70 + 9383169643224079599202758827539989065835783658435729888437438072394141) * 10 ^ 70 + 1740527598866340552281751199245313947802631597120642366706788132745106)

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

Polynomial.coeff recurrence4Scalar0Exceptional 421 = -(((535485875323484300947655259622546054319308928443 * 10 ^ 70 + 4090070299270281697880688073096793669678494487611498860149026797124336) * 10 ^ 70 + 8397923316177580768736321832708339249226857706470957115054217884112909) * 10 ^ 70 + 6590842792380761868950378561408742535399056518280531750462736521576243)

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

Polynomial.coeff recurrence4Scalar0Exceptional 422 = ((397508508587053891968141298940056925314501292738 * 10 ^ 70 + 4426546224465833593361885876890075427038724477407659248397992059767704) * 10 ^ 70 + 8277727215119221743931447189117916180723240555645357060257486448182358) * 10 ^ 70 + 9776800975892061655496778691158607942024724971822007443040246834376616

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

Polynomial.coeff recurrence4Scalar0Exceptional 423 = -(((162875151590448166703946490715910022688746465282 * 10 ^ 70 + 6535266197349472151186628149963982751451698870336768320806493886155003) * 10 ^ 70 + 5360890909640986999147531015528581973743772638615966497089072894857526) * 10 ^ 70 + 9492712511245176120151970048441429118305390604648933414373101317617298)

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

Polynomial.coeff recurrence4Scalar0Exceptional 424 = ((53256622987433692444109651195683865563041406181 * 10 ^ 70 + 9144407404826328184877415441710343503702221260819108216258119549746408) * 10 ^ 70 + 775630509416636548392451149184534013393854826522331158829176980094425) * 10 ^ 70 + 8778847097086824412771351030981005824927523133798318845801204046183473

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

Polynomial.coeff recurrence4Scalar0Exceptional 425 = -(((14965913629277865714870306320860172757008850739 * 10 ^ 70 + 9395594928932996545281727467423156288950059252144451917795536130036335) * 10 ^ 70 + 4506362930620074673427208201215419172457475131565427716054088710458622) * 10 ^ 70 + 2082277279723911008850412018867936042846801193477414295269335439210047)

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

Polynomial.coeff recurrence4Scalar0Exceptional 426 = ((3673244043569341370924820009832470482605622193 * 10 ^ 70 + 9803462817324321489632278051094322723543830560772841957510968899879390) * 10 ^ 70 + 2136065454691215159054888259398151625574019960372294483890102557939194) * 10 ^ 70 + 3631080143479163801981393271947156973206054172190983180199587272567972

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

Polynomial.coeff recurrence4Scalar0Exceptional 427 = -(((776097125264819482813350231528279377140991987 * 10 ^ 70 + 6586723604897731600290426680946272981776371568741565160999604778531759) * 10 ^ 70 + 7915996452840599533010343920998828863485811009123330678385937068109246) * 10 ^ 70 + 1057062924404154129858350504024311187405473152033728568579232358861328)

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

Polynomial.coeff recurrence4Scalar0Exceptional 428 = ((133000544790021722063332278525478325710513668 * 10 ^ 70 + 5593262191613228684079513817934259525885171886377457166833218491848748) * 10 ^ 70 + 9743966918310207453978760665393537438088275375064794721105338909012252) * 10 ^ 70 + 3205534715314874002899574437921692515572754698797869350417701151023729

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

Polynomial.coeff recurrence4Scalar0Exceptional 429 = -(((14706203468423096805955946506553615136190732 * 10 ^ 70 + 153496140208521648027543045211812647265804525830163557222842098757403) * 10 ^ 70 + 4032764845083546816560337831642226141914135809325416748079149317334821) * 10 ^ 70 + 3086277370989275484679957091741401629123006037314831207519678371572436)

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

Polynomial.coeff recurrence4Scalar0Exceptional 430 = -(((770962222664864907458159557301240792706016 * 10 ^ 70 + 1666032534922060397938834161590290432587330176491392721922249036520235) * 10 ^ 70 + 2674810942798397486304790451921898723711354059366011680472433236138783) * 10 ^ 70 + 3604988030707298716843966524768604970123515269314192103018613592639777)