Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar1FirstPart3.Coefficients408To432

Recurrence 4 lookup certificate: Scalar1First 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.recurrence4Scalar1First_coeff_408 :

Polynomial.coeff recurrence4Scalar1First 408 = -(((12314685739099620975860896360379613234942106121251067 * 10 ^ 70 + 491203118050764144335905889914474969898148244687878621385752682179587) * 10 ^ 70 + 5952939596071997627138389100751323271957193756800517959646629631770366) * 10 ^ 70 + 7129285628518049532729208439036854129286319510845475609475835077812672)

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

Polynomial.coeff recurrence4Scalar1First 409 = ((126094030961639835084911499362699075373938030502806 * 10 ^ 70 + 3563238178622721904475602054103387314463145290516033711046602745017299) * 10 ^ 70 + 7539670967817371839203612533101493168624223714557738903482192024788187) * 10 ^ 70 + 4526198348160514746041733769019642398728004828790494919343158444286335

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

Polynomial.coeff recurrence4Scalar1First 410 = ((1261144996264465699241456232569362526294220749464114 * 10 ^ 70 + 4854385389744970880949666450204246449449169203604411257525630944836748) * 10 ^ 70 + 4790700044655010580162247542678015723527386959575974079805027412617216) * 10 ^ 70 + 4318531524001897459105826465684887101500507659910374017998294478392726

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

Polynomial.coeff recurrence4Scalar1First 411 = -(((832578326569442170203503428575288387019851055342935 * 10 ^ 70 + 6856756299609761820769159537239681622687106863762339320078117448474967) * 10 ^ 70 + 2563168898785292935582501889440687945449707912114732765199287448146933) * 10 ^ 70 + 883044625708209621345023896949678093537868960049337106467251475110676)

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

Polynomial.coeff recurrence4Scalar1First 412 = ((405633917461658529955106442537298888721876050988260 * 10 ^ 70 + 6257194225674942751135934100848406812589047858396635543794544940356708) * 10 ^ 70 + 7390957701219051321351853312988387545724416797141841489728819012393827) * 10 ^ 70 + 1229558685573845029953359347103678028825589066741295891755389239293519

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

Polynomial.coeff recurrence4Scalar1First 413 = -(((175129248352031950367568626172171850928915623248721 * 10 ^ 70 + 9323729360025516027638882802661668953405589468981055750737104427484301) * 10 ^ 70 + 8303728918441634563239204852479786879912413781802739131557343299710762) * 10 ^ 70 + 5871114376928745671420476601367723195428334033484824627494671584863767)

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

Polynomial.coeff recurrence4Scalar1First 414 = ((71068665389949514774254619344485899375979720817465 * 10 ^ 70 + 3111637039350829058054046948681500794727183244202171359731212521719991) * 10 ^ 70 + 2770847764697588608509920474760194134993130960998318190966373292745943) * 10 ^ 70 + 3165343465221690722454825095828938585059153075698182973773857612590818

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

Polynomial.coeff recurrence4Scalar1First 415 = -(((27834010972262706447306443565527750713851726815993 * 10 ^ 70 + 4133609007963615917467710303419079540270712710930483618766780123395516) * 10 ^ 70 + 2696040407028547209898335527644601589311916863847932007139038705699973) * 10 ^ 70 + 8950021746110710383200202247763509428473440492276431649674828212000784)

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

Polynomial.coeff recurrence4Scalar1First 416 = ((10653112188201490388910657403193418904764698526092 * 10 ^ 70 + 612110698690949008501865573893788742986459144955735726696502003951116) * 10 ^ 70 + 5308056587210227364645468210747603974288321514533590336392471957885177) * 10 ^ 70 + 842497298834312224078930171073431998457333750963793811236535539827378

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

Polynomial.coeff recurrence4Scalar1First 417 = -(((4002859509429166695040939599159492825706589709259 * 10 ^ 70 + 3481227222484025945627106683104168859787411790311966289481892026925077) * 10 ^ 70 + 5769560478910099862368040303576388503218636237060475426569604787497709) * 10 ^ 70 + 4931285865364798940893362528886445851591948272307119555214641417809227)

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

Polynomial.coeff recurrence4Scalar1First 418 = ((1476118563612925448975140044625345148880346186120 * 10 ^ 70 + 3933310222608179193026554143855234070286079965843832005176473390401412) * 10 ^ 70 + 3082751439976855163773611764408144687744804335590214848706389799418353) * 10 ^ 70 + 1899756070116663489074695764128763128769571882720214503484222078575637

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

Polynomial.coeff recurrence4Scalar1First 419 = -(((532546780661737510224264188479387132480063730469 * 10 ^ 70 + 2819087271139037001550995347824746800643383076558265203465190960967051) * 10 ^ 70 + 5533560481734277587649504405380300235566348436113493594580882647409519) * 10 ^ 70 + 1488000706519842988414620598101744853071426735076472369210396071926393)

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

Polynomial.coeff recurrence4Scalar1First 420 = ((187112849634670669710045347961181346738007937296 * 10 ^ 70 + 1527235723999603459510087300264916719232134010882367529520785873928107) * 10 ^ 70 + 5318542909321838203270407022891920225746276688190440127581402107129491) * 10 ^ 70 + 9396116421564469112899803386568638689148028235025784665207760682111662

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

Polynomial.coeff recurrence4Scalar1First 421 = -(((63702355301096879307293242674104702974047304586 * 10 ^ 70 + 2189859477735125343932496233115402666691905230304474247774730783343492) * 10 ^ 70 + 6238393883261825228990307175905195964741283177366025028708439281983611) * 10 ^ 70 + 5333534936561251204821483599877389342653417353469474104284858685847814)

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

Polynomial.coeff recurrence4Scalar1First 422 = ((20903874329547241551944477327373204386858295987 * 10 ^ 70 + 7639778737365994564809643393999002780174397265545545109780657600427627) * 10 ^ 70 + 576670603025791184416795136359306972836415343396963965323987304969569) * 10 ^ 70 + 1984251044102986328033610785066826533091749347192295708461225691260931

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

Polynomial.coeff recurrence4Scalar1First 423 = -(((6574931811378281647287150358130890759458684964 * 10 ^ 70 + 2644728759879814005306634316018057674089370833134505757886843782808686) * 10 ^ 70 + 957051248550719409674419624413264148886686746761880617575433166937306) * 10 ^ 70 + 5379540712464073059522640782462244013888934855222229250599461691385365)

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

Polynomial.coeff recurrence4Scalar1First 424 = ((1969408069649551648669760350322372556059481701 * 10 ^ 70 + 7457321776674618216754865223112037122471871356004901198536798706950343) * 10 ^ 70 + 628949785018180332918100174176348607634244294087994802161048368695354) * 10 ^ 70 + 7684468788492534130736881286340706758568735339831459935338028642328335

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

Polynomial.coeff recurrence4Scalar1First 425 = -(((556993050167933241975068705441896131132744936 * 10 ^ 70 + 7874025919768391511892391673726626029342757745222840684741696779943335) * 10 ^ 70 + 4879995749888719256801526529517725346394468102677265448383214406899683) * 10 ^ 70 + 6866683335767896737008278033354764573596503529890106678596197851808715)

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

Polynomial.coeff recurrence4Scalar1First 426 = ((146818243655961183929081422081159288334296316 * 10 ^ 70 + 1232793750179516738566177621066918319901299315189813460958490334872471) * 10 ^ 70 + 7028427543965112671030972013545318661955081735247541668186706943588746) * 10 ^ 70 + 276433936169911095187710135509397277941009065668364790512493812847076

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

Polynomial.coeff recurrence4Scalar1First 427 = -(((35241793777768178260823436641252756735768406 * 10 ^ 70 + 2259808898090659142176180203951696777790485574783715026061855339877771) * 10 ^ 70 + 446204906840038030225491585500861297434379932996907671828241395976807) * 10 ^ 70 + 8690893496861929865666039025171121890083560730701544563293992041661860)

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

Polynomial.coeff recurrence4Scalar1First 428 = ((7325061108222872675037770520055189708283993 * 10 ^ 70 + 5807302855314584089624889951576483985685278119344422509335845781324231) * 10 ^ 70 + 2032762213538020225009186279631056851644701748260096917996736362637626) * 10 ^ 70 + 3323458566730419172708948740876950078136155823339629447982376322543370

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

Polynomial.coeff recurrence4Scalar1First 429 = -(((1130004530642996826581922239117057477063746 * 10 ^ 70 + 3564265967269146680637668517209474866626395314879361943436831207812383) * 10 ^ 70 + 4774013190024858324426789873932875597446292154805267664378242422861012) * 10 ^ 70 + 5488696314079257376469923623659357150203392793859860516326568092267992)

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

Polynomial.coeff recurrence4Scalar1First 430 = ((21053159365973591235619219175767840491349 * 10 ^ 70 + 6335475446623151487780580733072541228141212595651040009417615719950922) * 10 ^ 70 + 9725109152225720311987235096160575099802467396423817091132733968759946) * 10 ^ 70 + 4669404413082969540221680011944962880406000894933604329615817666811707

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

Polynomial.coeff recurrence4Scalar1First 431 = ((79599620568323515975148767013230774199049 * 10 ^ 70 + 9502493399342054907121272448589060601860189957479814247313628706733997) * 10 ^ 70 + 1151765277197106308599427188146878363970352087917324862514098139665005) * 10 ^ 70 + 2260084616645496212734756360397814449279092543928143419367725043245799

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

Polynomial.coeff recurrence4Scalar1First 432 = -(((44671674980263173513733185486935342783545 * 10 ^ 70 + 9381185907282987752361044073798624666566161192986342912371165627309212) * 10 ^ 70 + 3043269643145482557647032966017402695487434106821007120634159206121337) * 10 ^ 70 + 4868800498700953537236501411222313976546167961514819607211384815982394)