Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar1SecondPart0.Coefficients158To189

Recurrence 5 lookup certificate: Scalar1Second coefficient convolution #

This is a checked coefficient-lookup shard for the fifth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_158 :
Polynomial.coeff recurrence5Scalar1Second 158 = -(((((4 * 10 ^ 70 + 17021099747927190032403486443129518404168432979281976946639630007239) * 10 ^ 70 + 4398619834908788728760596564475305024433997483174831855067873387574719) * 10 ^ 70 + 45837912585916815091377240609159395801976271912381077965607980079426) * 10 ^ 70 + 1803869591225326004871897003085210073870309218275528063088885545727904) * 10 ^ 70 + 5384582816508201927481925530748557987245733973608532094790668026717482)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_159 :
Polynomial.coeff recurrence5Scalar1Second 159 = ((((9 * 10 ^ 70 + 5477498021159321498423007634164525537228914337738389704315243529451580) * 10 ^ 70 + 2057928667347074774529308115717997486956029217331601778572273671344594) * 10 ^ 70 + 1188781528650233599692748565353291460222878190627687957914792282904658) * 10 ^ 70 + 3361136947071092559667873256998505072706460961828186691015334183442005) * 10 ^ 70 + 9044968852777097305328402022264267306652969031571872517971651892158249
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_160 :
Polynomial.coeff recurrence5Scalar1Second 160 = -(((((22 * 10 ^ 70 + 3634272159776328603411939163696786393146604019135522106099151936625797) * 10 ^ 70 + 6671706543872449485557667193289830859751275898704298666985679525415041) * 10 ^ 70 + 8620502066411541285022200871921728952696565241227973446720493863702547) * 10 ^ 70 + 3668449533542849562811322385971902775114348712542587288111436059345328) * 10 ^ 70 + 7518477639963080828347110812054301551777933202254319873584875926854840)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_161 :
Polynomial.coeff recurrence5Scalar1Second 161 = ((((51 * 10 ^ 70 + 4267064351110448075740136752387894984530280797974153425966896166631203) * 10 ^ 70 + 8465045685658894212910928650448494681046360905459878537401709475302474) * 10 ^ 70 + 7996637693244731014098983956201635172118030860163829619782502161493882) * 10 ^ 70 + 1331405784238023288107728911965573181541228748120835618886015330171837) * 10 ^ 70 + 4268943591738989677904015709238913154142996414551336744418731377774878
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_162 :
Polynomial.coeff recurrence5Scalar1Second 162 = -(((((116 * 10 ^ 70 + 1136445227796019127655527868753708940688739348793802114739615502493920) * 10 ^ 70 + 3350823570211539398179271026349372703837421987138503468113126151826381) * 10 ^ 70 + 7997414337218954114381717217085803319874592569371741831763788484364198) * 10 ^ 70 + 5055209648945493382971338438384842037532619897715442186454251096613465) * 10 ^ 70 + 9546861289994786020131077058145019236785576994109942825543184392165196)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_163 :
Polynomial.coeff recurrence5Scalar1Second 163 = ((((257 * 10 ^ 70 + 4259976368143413366230716736445182246048135119493521555717465893451376) * 10 ^ 70 + 477501308768846878979082465766170417496946718046111087001728832108733) * 10 ^ 70 + 7968925061747172789695498842033607770451743016193533604395154817844961) * 10 ^ 70 + 1219987460047358354716539281133639221467554224182123358964680910795873) * 10 ^ 70 + 8128974077991567091644361097307626415612608416526562277200553428455043
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_164 :
Polynomial.coeff recurrence5Scalar1Second 164 = -(((((560 * 10 ^ 70 + 4357354998603049516521690483976772301440639877533058236607351068319645) * 10 ^ 70 + 9892105945228384119662287598327554603661458944525955296824031627521138) * 10 ^ 70 + 3573040963187242347393747110527716086521916418204309331613784868953777) * 10 ^ 70 + 4356011587184101255959787061680799495722756596504719103061511468506517) * 10 ^ 70 + 3965585154445060571695732530895970086057565754458127046579567198232198)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_165 :
Polynomial.coeff recurrence5Scalar1Second 165 = ((((1198 * 10 ^ 70 + 2086417737806641803274103974037717438373061452132023319703305328290191) * 10 ^ 70 + 8179364429645363677470306300703291950069258357658799515208440199124001) * 10 ^ 70 + 8238641099133419316540274567958994577453328327975822243666370040811438) * 10 ^ 70 + 187731068716015693439132392498181391638642024779306068960909708905763) * 10 ^ 70 + 8837421771129520398547294765438465387855978825522040706205773521209159
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_166 :
Polynomial.coeff recurrence5Scalar1Second 166 = -(((((2515 * 10 ^ 70 + 9414789275112626300919139809918196223611145507721338443775549255195792) * 10 ^ 70 + 3471494566038743626750959736751467254609717801413585342071338379168109) * 10 ^ 70 + 8649291084701001852108995086770505221903721854253761257070789122715253) * 10 ^ 70 + 9234936457553183214882375449998635672572241595050369142657023783866124) * 10 ^ 70 + 6276739682277371570726466591400123652473828841011086587030541558479262)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_167 :
Polynomial.coeff recurrence5Scalar1Second 167 = ((((5188 * 10 ^ 70 + 6891670334105282996069445878080367674475231027637796226450534075784770) * 10 ^ 70 + 9338894288129084855656854139299531778582768995146456806469608045561022) * 10 ^ 70 + 5896229921258682904925586777381213906860577179802237785213368366383107) * 10 ^ 70 + 8579508386899383254253164168015247751636003776467753620488675543322165) * 10 ^ 70 + 6796780398454225455619903015264454473200294174373070552435873145157397
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_168 :
Polynomial.coeff recurrence5Scalar1Second 168 = -(((((10510 * 10 ^ 70 + 6778332815704666160427454261877678425505760828328758442763317037306199) * 10 ^ 70 + 8980500371562796717155189786971401690793150015803298014562473051361697) * 10 ^ 70 + 2029120136333041861151606735736022873338951966358337750877505970142178) * 10 ^ 70 + 6943491120109077292165358491045722997526506198680793783915971116622573) * 10 ^ 70 + 2500962230774174725968647635033118175567901686164203745438253977242172)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_169 :
Polynomial.coeff recurrence5Scalar1Second 169 = ((((20914 * 10 ^ 70 + 4299346765253884480948854304934161162028036741850283292174074361750483) * 10 ^ 70 + 8823480636470125187249448068382408860815663023716224952487300740581766) * 10 ^ 70 + 6423841009069326445962561898343547355911158383015612257226075490373408) * 10 ^ 70 + 5484185759023118295696117016897006949300205386477965971494951196614747) * 10 ^ 70 + 9129172809177681822634406058130797881586616274326340974262399076990847
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_170 :
Polynomial.coeff recurrence5Scalar1Second 170 = -(((((40881 * 10 ^ 70 + 7287068470861535258157569158807620336104326937999638819294495254861422) * 10 ^ 70 + 543232299950225727129555200247447488009073495945141254839502184920904) * 10 ^ 70 + 6673566048735299772283295152678918753319521944634157529882952861319488) * 10 ^ 70 + 124011000677060070462029501253515754876128533222435325402789311183630) * 10 ^ 70 + 5600379433438759199789261107333945872178526359332423535638850142817852)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_171 :
Polynomial.coeff recurrence5Scalar1Second 171 = ((((78506 * 10 ^ 70 + 4742192522131989928392066224579012325162683691294118579055365979516857) * 10 ^ 70 + 5866570861082016288270739044867382459935943694511967508809152304159689) * 10 ^ 70 + 7019667824586050292361249503804938048233901161478033885561805468688599) * 10 ^ 70 + 7053602676355910698927170418362855745335648620907503692550329600727007) * 10 ^ 70 + 3032665347496040890647473090732797728752287233544144072864676712563366
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_172 :
Polynomial.coeff recurrence5Scalar1Second 172 = -(((((148115 * 10 ^ 70 + 589389636804208681369868869850327817218787967426340412977711655497030) * 10 ^ 70 + 979093969989669738251467326891838377225507892438740587141248721647172) * 10 ^ 70 + 6462940945752614993397533697991000966376566271570504181159464347411179) * 10 ^ 70 + 4828580297263368211436454361129925021508593001343710218045663056017119) * 10 ^ 70 + 9209732925482023266497951912959734623415185920360297752208847578296886)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_173 :
Polynomial.coeff recurrence5Scalar1Second 173 = ((((274558 * 10 ^ 70 + 2212724926919017600000300960543923225916882007002852242548117276867393) * 10 ^ 70 + 7188541397935302043679667988550350385463742071778683278823910614948206) * 10 ^ 70 + 5247735156275577212053577209562518670108654680839417668322381060859308) * 10 ^ 70 + 3847635152743656579397265328551463485212265926654206476980736884030591) * 10 ^ 70 + 258901070166645415983216006733381854087106697793656353289050538512765
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_174 :
Polynomial.coeff recurrence5Scalar1Second 174 = -(((((500074 * 10 ^ 70 + 4110504716343403533066455689557680194761592377755170422969765160815416) * 10 ^ 70 + 4156527216676757257656080611937431378691680587135725443819111988861936) * 10 ^ 70 + 7845785263607682519046304576402770457637000741166010161594504038415745) * 10 ^ 70 + 2120284259769312700983315553140344733967545398121907360322864009845392) * 10 ^ 70 + 8054884917239491161843033290091764099096900009360093846519725300400364)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_175 :
Polynomial.coeff recurrence5Scalar1Second 175 = ((((894999 * 10 ^ 70 + 3054830174240891862653215448088834159865078639116252561160167808090554) * 10 ^ 70 + 8123137158505673144182788694196958068486915171651384233542624067038932) * 10 ^ 70 + 8382489702285233881793388394992237623703725103975642269431239085529408) * 10 ^ 70 + 2097634332386588072015632659457205987690544801663620565887050097299947) * 10 ^ 70 + 9850985257806967993007434826027288429615854461089744505052009652745150
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_176 :
Polynomial.coeff recurrence5Scalar1Second 176 = -(((((1574059 * 10 ^ 70 + 3803375506049375062796027268579168766953084852377444738324704432037016) * 10 ^ 70 + 132702923940394933413231254218488827420732667612838227451460593103868) * 10 ^ 70 + 3659039646874991913329173570922788411537618865126593366557776231690293) * 10 ^ 70 + 4356859463783357906060611210366900749101185364691920148877493971677028) * 10 ^ 70 + 5270067742908237365835029234143991973839307138374787256051524224082683)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_177 :
Polynomial.coeff recurrence5Scalar1Second 177 = ((((2720519 * 10 ^ 70 + 6752143432336720826997031441793628551076373295572042548013494799521882) * 10 ^ 70 + 8831551244189016753024279118216781095510080989253327716436440388748218) * 10 ^ 70 + 1048237999964117164256277982203990751344973445132151034381040057370044) * 10 ^ 70 + 8947250199014835716668880835487748993800542085615262044568635034116942) * 10 ^ 70 + 3532359572129133275740873308691484577330118576571251241251196471189112
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_178 :
Polynomial.coeff recurrence5Scalar1Second 178 = -(((((4621006 * 10 ^ 70 + 122207201707637997944059417552263490643920762867795532815389371660367) * 10 ^ 70 + 6314543724220327276136491366988905493864540376594905449371813250592022) * 10 ^ 70 + 1854077380080378697887955857971359494252724480121774936821803725798170) * 10 ^ 70 + 1547871605416707719117024560300348584276335223170471728774127311673522) * 10 ^ 70 + 5114357477382595340014385370616800505657561217523609147296358678090923)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_179 :
Polynomial.coeff recurrence5Scalar1Second 179 = ((((7714294 * 10 ^ 70 + 8829606267969070410182663017785732891894145702156328719031530274223819) * 10 ^ 70 + 6615448658348700839520680627848498386556303997361552173331213266316022) * 10 ^ 70 + 7280300976155232736014518924594681958797045996497466233641307892025996) * 10 ^ 70 + 291354029832884024888042942620875056552268735294707667012469212312153) * 10 ^ 70 + 8479113196624061223479320084326946136970168446256458828714366267369090
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_180 :
Polynomial.coeff recurrence5Scalar1Second 180 = -(((((12657610 * 10 ^ 70 + 1597215340963871053767832271478989736506192034330568300283788538000890) * 10 ^ 70 + 113662916075506675718143445663074274094830976755373872850636441317623) * 10 ^ 70 + 6068589716388669148311299559421728011199961707503715797929589920951944) * 10 ^ 70 + 7296322107446509754816478858617518953923764298241224635364235743051981) * 10 ^ 70 + 1211537157192427840196149711656161200875108154714726903860037474730427)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_181 :
Polynomial.coeff recurrence5Scalar1Second 181 = ((((20413775 * 10 ^ 70 + 3629657918118206059677661751912667139439365842420157668503694195579930) * 10 ^ 70 + 2456318598275753347849184415553626226202325550314523283939605206791308) * 10 ^ 70 + 797545198514837482273396601068259107727601959107006952779903733530395) * 10 ^ 70 + 3556050535984638635541059343909776323507665097968137376949264516864781) * 10 ^ 70 + 1685014387572561627100940789137105232171429260740123300884614182874965
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_182 :
Polynomial.coeff recurrence5Scalar1Second 182 = -(((((32361681 * 10 ^ 70 + 7771281914181682156757676661820951480496134325511895239606709968028885) * 10 ^ 70 + 8997595951571117812870515691584905402576065720182757326928119512049068) * 10 ^ 70 + 7449743018400676764279441436391038327411801885711673755028580524473855) * 10 ^ 70 + 3554559549405684348290223873897066222791021966162612640242382601703774) * 10 ^ 70 + 3114782900014822446563157888705652487829130782397631979311411679764895)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_183 :
Polynomial.coeff recurrence5Scalar1Second 183 = ((((50430657 * 10 ^ 70 + 7344355521333620186703938664371530049138843791330285056075053553313349) * 10 ^ 70 + 7475383965377637752201935259569419243364114799406576835215650574228289) * 10 ^ 70 + 5920332057262454250669211687658176333953636634483320750561876512959899) * 10 ^ 70 + 2731974293452378374328935868005194087821024809349632912001377817576825) * 10 ^ 70 + 5156545876062157126868795291901010044437901199292545469805366336076931
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_184 :
Polynomial.coeff recurrence5Scalar1Second 184 = -(((((77256196 * 10 ^ 70 + 4731705818852595556339577898543832312595535754372701026601706379757473) * 10 ^ 70 + 6107880724131955400722756922652925339506482048390939509155315997150940) * 10 ^ 70 + 7144546506560687044474864465640153303712621145791699947750007161768394) * 10 ^ 70 + 7352654394935093806428201750687491234765104429847893714051674678597792) * 10 ^ 70 + 3142726912567427276773482689632571205449242872332999335678822196992803)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_185 :
Polynomial.coeff recurrence5Scalar1Second 185 = ((((116349949 * 10 ^ 70 + 2313139217134265493821413397841262643158385619793853536957780724482638) * 10 ^ 70 + 7102600608207502845995332967702935509029540330191964983170546433962394) * 10 ^ 70 + 7267292496821471447160538953508711490625631927116120070369790546503761) * 10 ^ 70 + 3676730724975497566427761870144142400383400275534393627267032581110195) * 10 ^ 70 + 9484137685400167197713312683605794318771340184346035253485686429359213
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_186 :
Polynomial.coeff recurrence5Scalar1Second 186 = -(((((172270938 * 10 ^ 70 + 9014178894400205987373294241980012613243129119609888613069975383861621) * 10 ^ 70 + 5383607794944171987575266723080830248032152297100870870567076445962454) * 10 ^ 70 + 7810934936513986776483900139215711073660425060985766281341924842974865) * 10 ^ 70 + 1417478399671258145481669956326343249730490427071940937845315586812949) * 10 ^ 70 + 4623520092799029682294493900549631314339343517821706724950672091732121)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_187 :
Polynomial.coeff recurrence5Scalar1Second 187 = ((((250777916 * 10 ^ 70 + 262672372995632736865411624836820035834683715955087504595059172829946) * 10 ^ 70 + 4525021875604853503153318886486560869903107860498348826161008303465307) * 10 ^ 70 + 8299616509903939369941996096687888189273513782145229048360847719024214) * 10 ^ 70 + 5226188723294197654998252156416730128734737770673078205725922768465793) * 10 ^ 70 + 6851164763385417582308299478579696002235332646645887567569930475504409
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_188 :
Polynomial.coeff recurrence5Scalar1Second 188 = -(((((358935367 * 10 ^ 70 + 5346147433004899243283601999465928320092702648213442349262163688479423) * 10 ^ 70 + 1278274839998166777754591627642996451890805579665001100274603822067885) * 10 ^ 70 + 9009867435654725214381755513028436039952841149051312035885023100070884) * 10 ^ 70 + 4404599151324009541432657681419663249563619854849598145358923186957416) * 10 ^ 70 + 8428973293289521944826665425608406183685434909729188360558694646184996)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Second_coeff_189 :
Polynomial.coeff recurrence5Scalar1Second 189 = ((((505139034 * 10 ^ 70 + 6302580416013657989087065695369456148727678993555745911001181083000685) * 10 ^ 70 + 2568874012890054749937543242339609726691519021890646078903499308082855) * 10 ^ 70 + 9810378983785316099832184148397784060909693279336264658458270115861747) * 10 ^ 70 + 1747372576740291780088962667497312629757186869273983009054765778526893) * 10 ^ 70 + 2581612062013548896311630804312963888071695738807421399614012779185425