Recurrence 4 lookup certificate: Scalar1Left 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.recurrence4Scalar1Left_coeff_324 :
Polynomial.coeff recurrence4Scalar1Left 324 = (((30579051699658885 * 10 ^ 70 + 5513895268853522234943644876529411444356416817121882613730757224773257) * 10 ^ 70 + 1510712758210098313622086906459803333614964035194201862817756660421156) * 10 ^ 70 + 4724451806960401798652151427474369353729664545153372251926854126041828) * 10 ^ 70 + 5502388501826598749394371007211453792762656253433752806937816659088084
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_325 :
Polynomial.coeff recurrence4Scalar1Left 325 = -((((30381930179249415 * 10 ^ 70 + 9524418668185145439671530770405873481990559828543003894390423769690423) * 10 ^ 70 + 5537315334000286969217537978388408594117074866473327514532702091692150) * 10 ^ 70 + 4372356447006964420420290480061517788674070008402702900650757808281929) * 10 ^ 70 + 5915880384046744646945666091107184754748312531770244334138877086801098)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_326 :
Polynomial.coeff recurrence4Scalar1Left 326 = (((23195013159806227 * 10 ^ 70 + 3380448689038159202874732612029599831846643100947974284453952067377694) * 10 ^ 70 + 517096823045240028749079907077856059116659448711453390815432530094314) * 10 ^ 70 + 6860497901001877418530817588637599519067310118406403986798436637536183) * 10 ^ 70 + 1399541471923285712792052765638010666338551984777274144193163167669243
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_327 :
Polynomial.coeff recurrence4Scalar1Left 327 = -((((15688945630511665 * 10 ^ 70 + 7350752345542952368474894187857819057559000957385713088663982109646983) * 10 ^ 70 + 4669338091457481422059348870994912160017828927065357409724694501210299) * 10 ^ 70 + 6236570121361983986722171036289654289274616275410895828669775166883166) * 10 ^ 70 + 1597369496925709391757720037921558483839601720351158982251463034674633)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_328 :
Polynomial.coeff recurrence4Scalar1Left 328 = (((9859091026544070 * 10 ^ 70 + 7366975950690620124732256746922687111685371729241069274449426559475348) * 10 ^ 70 + 2344795068481708662776765721960878132895532386461004201369526563702187) * 10 ^ 70 + 6142787728259442412977208062689395271341184436124780339444138375157183) * 10 ^ 70 + 3248323993379951970990340623930281408442804205462735485124989844958560
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_329 :
Polynomial.coeff recurrence4Scalar1Left 329 = -((((5882509406296779 * 10 ^ 70 + 3294669478765850329860529049364122220563511617512885117280143109850647) * 10 ^ 70 + 2019601529430886635411066528146453100057425799371892725405680165981591) * 10 ^ 70 + 2074425996598470398764649327756563716327424100778036242541426089674069) * 10 ^ 70 + 3970905856292056293620667116064554037416700034938483564335670291556452)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_330 :
Polynomial.coeff recurrence4Scalar1Left 330 = (((3371865490747043 * 10 ^ 70 + 7924908554061287136749465213329432641509780804498705771087501593552873) * 10 ^ 70 + 1704946435375132572743993913364591701692054533792287086383596036437278) * 10 ^ 70 + 9042933681833590064652279593874797712231726455201342737071735475160038) * 10 ^ 70 + 4110496432209455991535939947599514594281477416918835760383261143520021
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_331 :
Polynomial.coeff recurrence4Scalar1Left 331 = -((((1869868695295900 * 10 ^ 70 + 9689678398648764983046998140683603861680046607427177283331258896528901) * 10 ^ 70 + 2190067311956919866067821803487728102640713033889273116906961637464676) * 10 ^ 70 + 6552003745599665772877070328361101939535503007803597440538917958219904) * 10 ^ 70 + 5469260118326920264011213526762245831187024194124661589155069926880009)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_332 :
Polynomial.coeff recurrence4Scalar1Left 332 = (((1007716174659003 * 10 ^ 70 + 7079655937116559693809692127283197025913390955951880732704357783391215) * 10 ^ 70 + 5056267739571221462291452434431491704438715856292222517344282677935721) * 10 ^ 70 + 8244866612913319089442783508215280228966795219708104171833935441556428) * 10 ^ 70 + 2904534633866517047157867048806808058088977660533495893879459897546034
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_333 :
Polynomial.coeff recurrence4Scalar1Left 333 = -((((529368849940067 * 10 ^ 70 + 8330461526729872643130336548459537796854339339783464422338360121282547) * 10 ^ 70 + 2183505405580020111593734455904399572888829766242761552240371935362561) * 10 ^ 70 + 7461504785397702192664107434522973235056673543103157832447943069721118) * 10 ^ 70 + 1612540263406663568370053307523175850657986912564661742612517105164271)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_334 :
Polynomial.coeff recurrence4Scalar1Left 334 = (((271625118684423 * 10 ^ 70 + 1335790303530192928919069194040771750995999878149556736191539951231123) * 10 ^ 70 + 7076604845921952223171878616126180027418176983003599680788429594947907) * 10 ^ 70 + 7472096512869455932426889878874108382414682320243860783104738546899340) * 10 ^ 70 + 1892276454135685924899985070183799362852777338935232261249967773267921
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_335 :
Polynomial.coeff recurrence4Scalar1Left 335 = -((((136331852337229 * 10 ^ 70 + 5402304403099714244776644841631884934382802757830116186393912101819944) * 10 ^ 70 + 4703876843581930767890183644386782613600130261835987871256247188867538) * 10 ^ 70 + 5384615248178316222936260769231729098204266394974926934352037889551546) * 10 ^ 70 + 7571979137438071368039271693188997653576096804120009673139238320106268)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_336 :
Polynomial.coeff recurrence4Scalar1Left 336 = (((66999500535268 * 10 ^ 70 + 4109769534057254689329484194317947242069233284139274965792547440194162) * 10 ^ 70 + 1148617713878801847007861702178886636139489600265815211271217177011740) * 10 ^ 70 + 1433508534212444508041309025051061878428770804119510056147523953382596) * 10 ^ 70 + 3229331420722056305786977090434604554347754400478669712821468762170929
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_337 :
Polynomial.coeff recurrence4Scalar1Left 337 = -((((32261164232005 * 10 ^ 70 + 3480904964042819123708358085797784237076166314399421172618230717285922) * 10 ^ 70 + 2833330981071406052670793957421803100997216631660768347544853933790328) * 10 ^ 70 + 4368278970836009234409194782436768290109249613052557329711508991722894) * 10 ^ 70 + 8254176384693086164860834529510157067356884009852568690053623331845176)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_338 :
Polynomial.coeff recurrence4Scalar1Left 338 = (((15226440301887 * 10 ^ 70 + 4796153614000863454535752663883633587845294052264872360059707630779566) * 10 ^ 70 + 2616840726961423855769880210116639513612972799864297647945284129161294) * 10 ^ 70 + 6003768072770500784397914476548514726405576890514288390967391257813647) * 10 ^ 70 + 8670156909912973588834703589947157383521093477654213158342857814665614
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_339 :
Polynomial.coeff recurrence4Scalar1Left 339 = -((((7045481744280 * 10 ^ 70 + 3165262550058909392944267582658267160942863665998971812242380315007072) * 10 ^ 70 + 3567643788688382538949021806237994171944973842873186174870680925228219) * 10 ^ 70 + 5246777701136655702691287351865922453095095723746965958433598059453059) * 10 ^ 70 + 950268697122181024067807029913980904929474288936492964541650045207373)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_340 :
Polynomial.coeff recurrence4Scalar1Left 340 = (((3196111641972 * 10 ^ 70 + 7826487887046743458489775620746202322459933141285432091215651017507864) * 10 ^ 70 + 8174561687111051278851063422752447297220635024444022506384753507045140) * 10 ^ 70 + 5380921583448875582963855992135290732011543978996518613013394167652254) * 10 ^ 70 + 2361137357832812826517734645151730677945267069903196716202601366811886
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_341 :
Polynomial.coeff recurrence4Scalar1Left 341 = -((((1421231313857 * 10 ^ 70 + 249849655771272954005547909444618553324141222918378950753396462295969) * 10 ^ 70 + 740318465764999686446202475307082056234618704900770637917212762097107) * 10 ^ 70 + 4658363466969751770672211550242230356306373282380429765740787922169244) * 10 ^ 70 + 5914938732126477602018718586227043923432026150700397584914060820566036)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_342 :
Polynomial.coeff recurrence4Scalar1Left 342 = (((619300938810 * 10 ^ 70 + 9669843547419090852130540001335760459491344384763289096576765953868277) * 10 ^ 70 + 6538881781458637817137603579800419456962997826018515431080588779675961) * 10 ^ 70 + 9005893015695147790397735921050458895842796562400715481277244875998475) * 10 ^ 70 + 9164576046225989599174287320802550782348941415895665006273786167679846
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_343 :
Polynomial.coeff recurrence4Scalar1Left 343 = -((((264316071371 * 10 ^ 70 + 2145686266753652200473426768167320920665395977074265835718894855646161) * 10 ^ 70 + 1098105700033954518432911041474931272649596741883786333784503501964746) * 10 ^ 70 + 8067208192200601597119318464301262320076400278414555062976163461093953) * 10 ^ 70 + 9999023495864840733916593328475444758425864313934435973910287670803813)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_344 :
Polynomial.coeff recurrence4Scalar1Left 344 = (((110418876561 * 10 ^ 70 + 6322090269962453347639029256271228463799300244391979158692245260168493) * 10 ^ 70 + 4301226450985615745363370914259789293503438330329512862242699949663731) * 10 ^ 70 + 662651688101608948506963411398518579980896599006672396130370316136546) * 10 ^ 70 + 562567539056854872709523343473927240363735476321949475839782577935264
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_345 :
Polynomial.coeff recurrence4Scalar1Left 345 = -((((45111371729 * 10 ^ 70 + 8617888303501166839701047908022980215901759921085353027658258687505268) * 10 ^ 70 + 494721840349199970468713430099288262817283524376680453592282141603198) * 10 ^ 70 + 2963434179622912613259486995455934214834464586840645291701920537666487) * 10 ^ 70 + 1235476218084469483949969491557739492689224378573578877908885176764766)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_346 :
Polynomial.coeff recurrence4Scalar1Left 346 = (((18004151386 * 10 ^ 70 + 6909651783875763611600447945552380115641940145728134145584732823230991) * 10 ^ 70 + 4613663635372219819932316943349415059259094310453483351514014706622795) * 10 ^ 70 + 8869373888217170179873173492043598606503615597009241310524928025183799) * 10 ^ 70 + 9926791516478751904442020544963409544471468678035781497265566016017879
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_347 :
Polynomial.coeff recurrence4Scalar1Left 347 = -((((7009649967 * 10 ^ 70 + 2794997947836589263687929839325940648161819787930170197572684263281560) * 10 ^ 70 + 7198468864357585312985978304819848421316819415638256143729696558266620) * 10 ^ 70 + 6544601763651806789213680898267087704451100647460041528179783905697846) * 10 ^ 70 + 9140950206497509098126197402510031339737110611508727154567372450201322)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_348 :
Polynomial.coeff recurrence4Scalar1Left 348 = (((2657586926 * 10 ^ 70 + 3166073884875841189697622966327627356509039186891039963551899176693776) * 10 ^ 70 + 9383695151531740333302400571099402658707831823484087223005285447542111) * 10 ^ 70 + 6395523504156681591824036871629395264256878600851649230926688073091356) * 10 ^ 70 + 7355371960674811593694250638847494022159454740629756888569570773665079
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_349 :
Polynomial.coeff recurrence4Scalar1Left 349 = -((((978952660 * 10 ^ 70 + 1132333624247932095290090604508237582980913475057099561143342092135626) * 10 ^ 70 + 9078424452795105187835827229608827376651192817986501114313185233087734) * 10 ^ 70 + 8473274614935214620670931170977498001095877699795776468889947558936139) * 10 ^ 70 + 5671171555926266780901863962586311404474722347498440002724001603399230)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Left_coeff_350 :
Polynomial.coeff recurrence4Scalar1Left 350 = (((349332866 * 10 ^ 70 + 1487798874933734401974904029100840130475212804922410598093190064875393) * 10 ^ 70 + 3549306224056646348176914112663293244529331463733138487352259798033386) * 10 ^ 70 + 4367539753245060977003831060978767834067039948311212160466227198484992) * 10 ^ 70 + 9142907502693119288923267411259154340610670670886013282361087242785659