Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar1LeftPart0.Coefficients193To222

Recurrence 5 lookup certificate: Scalar1Left 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.recurrence5Scalar1Left_coeff_193 :
Polynomial.coeff recurrence5Scalar1Left 193 = ((((2970785218 * 10 ^ 70 + 9958721733434232339443218813154970842480804192650266215862529918200782) * 10 ^ 70 + 8006446947257157190212178833558795337017153582943699994587017092406573) * 10 ^ 70 + 555317638047378436665781862750646323826236232653216115389651977272100) * 10 ^ 70 + 5845174925483012724289280838466781092221035716983336556761532341011777) * 10 ^ 70 + 8287875598783038843072211690054107856355425037680808680395452636458418
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_194 :
Polynomial.coeff recurrence5Scalar1Left 194 = -(((((3838059910 * 10 ^ 70 + 3031808923822866971124891715609948477642250870701863189885030375663416) * 10 ^ 70 + 8210991754155336499821429399519277265230465131248519868938139959917416) * 10 ^ 70 + 9645116098137510363533616295452135171743000385237774435616011334894672) * 10 ^ 70 + 7520934703149013402152896508517970639935637231641740712388584817162875) * 10 ^ 70 + 7452170252381825963092129223322374867280183945950331697660774849798693)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_195 :
Polynomial.coeff recurrence5Scalar1Left 195 = ((((4873522965 * 10 ^ 70 + 7259313961546992344960731376409399511806476338383039101255480103227203) * 10 ^ 70 + 4240109290643811701818018162638632830264127164156658929101472414281030) * 10 ^ 70 + 4424984207901516922689501547502274478919410241193300459648032755536070) * 10 ^ 70 + 6855131121935380992991168823760454822930781896956272606203695901728657) * 10 ^ 70 + 2167305623976856896307016634655158781219837360679754649495559187061635
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_196 :
Polynomial.coeff recurrence5Scalar1Left 196 = -(((((6082113400 * 10 ^ 70 + 5736339350841993210994385234478108784592904118355303879583123728350794) * 10 ^ 70 + 2618257651144835855376236984425242391093176284278379037494357626499947) * 10 ^ 70 + 9384927749917024468298312143465041080847103746670287105741685984966353) * 10 ^ 70 + 501217738336475457862156999440256710708203164291810193522958994297178) * 10 ^ 70 + 2220497322841985524516659987717460796418527918512804338704672451891026)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_197 :
Polynomial.coeff recurrence5Scalar1Left 197 = ((((7459900207 * 10 ^ 70 + 4704026290114958193365463802198474610988819666588996890695134527320914) * 10 ^ 70 + 1538403161758673335999710772156025952347735099174032536652140733971087) * 10 ^ 70 + 6760459580685988782170822642867584601841511247468282516912722826795404) * 10 ^ 70 + 922488570474394739354781081552976280063911802820413982539991928803110) * 10 ^ 70 + 2205693332116837455548096274084176839520825257397315096981144665617006
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_198 :
Polynomial.coeff recurrence5Scalar1Left 198 = -(((((8992125056 * 10 ^ 70 + 7227868584539047439045370557430167435906634618509689774002397267196057) * 10 ^ 70 + 1957238211234689652471261843812014908790497680344170324795444128776411) * 10 ^ 70 + 9844191760620342915151009061184787404827073238728508898945707422524713) * 10 ^ 70 + 8508046095233023777543411294133187530520206778079468459498635904507974) * 10 ^ 70 + 6514431022590020617499795521461717758547434314227067501109139228799467)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_199 :
Polynomial.coeff recurrence5Scalar1Left 199 = ((((10651799012 * 10 ^ 70 + 4217283577198090089162862588088820234846756033859360707290508908262001) * 10 ^ 70 + 1959866456529589237909723189489925239939844969322742905862705333266991) * 10 ^ 70 + 8116530703636953952898417834938841285375030692576598815325081628147438) * 10 ^ 70 + 9741926538859736535084792387455126773335088944658958655402752202087361) * 10 ^ 70 + 7529952942665461262449974703652607044604737155882770873311842640521821
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_200 :
Polynomial.coeff recurrence5Scalar1Left 200 = -(((((12399142582 * 10 ^ 70 + 7705220671262025097937930517196102402066448722520043067983290694721358) * 10 ^ 70 + 8740480869417744594608838381597027909680637336427442247982308911757295) * 10 ^ 70 + 5792295687882874022791135083318208428765696196657808475192741429452334) * 10 ^ 70 + 5265111800002389694320424864378634330815836688208534877981111359692666) * 10 ^ 70 + 1340102618870379136360283340627521449475678678045031824487569873279575)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_201 :
Polynomial.coeff recurrence5Scalar1Left 201 = ((((14182113536 * 10 ^ 70 + 7454979246472530042358575638384040885979118070675473290295879221355902) * 10 ^ 70 + 6688421418640335759354671430480282631714399420372959747186109147338705) * 10 ^ 70 + 4083262903198952935219566738214029346628765711021069473901296362968840) * 10 ^ 70 + 6927711112588468214622692876665643717978350927520227649096242366744774) * 10 ^ 70 + 9560036074138257805693666773578057160038566093437686631622072600408375
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_202 :
Polynomial.coeff recurrence5Scalar1Left 202 = -(((((15938176265 * 10 ^ 70 + 4727493264491200028427581930213306698189286703100184004556595246273455) * 10 ^ 70 + 4515302123957354227390325860250222945204250049364308899462215592119101) * 10 ^ 70 + 6290637420147061403043720961289186815775600495352352713695990476130123) * 10 ^ 70 + 435765116540452258687922827795996004631327059589205758006759755670620) * 10 ^ 70 + 7738187384263229851975698670350551345359406954192205428439407022608606)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_203 :
Polynomial.coeff recurrence5Scalar1Left 203 = ((((17597335518 * 10 ^ 70 + 3664053495778763353182523058905752630682137831033729152367949510926229) * 10 ^ 70 + 62386055577726611142403214494616714872090646217888485388333821944528) * 10 ^ 70 + 3474184965843377773834173914925342062631216211248636175064886336861405) * 10 ^ 70 + 3906628090350253846904303905901653791949086905549144027447765298296649) * 10 ^ 70 + 2194465196072922721633637095315028339072985794340408190981468134589761
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_204 :
Polynomial.coeff recurrence5Scalar1Left 204 = -(((((19086299928 * 10 ^ 70 + 4719007419731700851625272439269565651454673064442232462045314179958961) * 10 ^ 70 + 6187651102355959222152139720006806967547045364272148439463739712608782) * 10 ^ 70 + 3878415975015330148590858361726994387376496331599516619873779285756627) * 10 ^ 70 + 201263865046807076224900856321694761204913870801418818655298371809055) * 10 ^ 70 + 9854069137823906635137929872046777249839167477233720790757912480616319)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_205 :
Polynomial.coeff recurrence5Scalar1Left 205 = ((((20333477877 * 10 ^ 70 + 780754384702656608337441862889594311906231328296005894540786040390159) * 10 ^ 70 + 3040948420058792184422818147597742324691846760545446238467814049310273) * 10 ^ 70 + 2509436971249528055905993959973023145920399363998991625032382892353857) * 10 ^ 70 + 2745362119280667144028871754900065913444528328924416204084495443110023) * 10 ^ 70 + 1870756954452847605921308000272027150756470909868746247552525317092124
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_206 :
Polynomial.coeff recurrence5Scalar1Left 206 = -(((((21274365246 * 10 ^ 70 + 1928771579576181067904333474029189094963089384365952596527546744422815) * 10 ^ 70 + 5006054034777229951284767793302870716872860400198996482287415574338443) * 10 ^ 70 + 6381667421286649010508061872027775875614193289178450070603506252057624) * 10 ^ 70 + 8667183630812417425193338458638959746022258943227502779678723978367554) * 10 ^ 70 + 9966499080433230685979802852121930869382735993617111460917120723352809)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_207 :
Polynomial.coeff recurrence5Scalar1Left 207 = ((((21856786812 * 10 ^ 70 + 3597290782214578589873497715975025813259223496086890503730816041052469) * 10 ^ 70 + 5797476706987025215244036942546672539541610714858195818087135166933329) * 10 ^ 70 + 6570466570781327234565775382079032126133854900318397773961602492299010) * 10 ^ 70 + 1090306444832963934315614447296110390531626519390123509156911030611838) * 10 ^ 70 + 7106335633719992612394572736077928845752779510506198651313548324388868
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_208 :
Polynomial.coeff recurrence5Scalar1Left 208 = -(((((22045420958 * 10 ^ 70 + 810821222183551104124621339777340224771644359833758062155768915801441) * 10 ^ 70 + 9057980063292805260297054208318675651383317133231689009469778287673907) * 10 ^ 70 + 9435394557810601046880958779649637107089238208087272865924779763740288) * 10 ^ 70 + 8125891711252391601249225613402060706213869869948866277981841456596537) * 10 ^ 70 + 6571352997986762637977564844134887550910490904932106420880932358943672)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_209 :
Polynomial.coeff recurrence5Scalar1Left 209 = ((((21825082244 * 10 ^ 70 + 6447146541112483026515500188024368267467684386702439164885748695677008) * 10 ^ 70 + 8858214712050617521498530601677702464442626388929877426527102830090008) * 10 ^ 70 + 338753670974556342819503109096899065526702233741090220893954928820168) * 10 ^ 70 + 9492079578007906218861990204597471769963805098565867841106976048273335) * 10 ^ 70 + 5716665984934019529047689386277929204052454716308227919472163748745517
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_210 :
Polynomial.coeff recurrence5Scalar1Left 210 = -(((((21202357140 * 10 ^ 70 + 3413107336121068669073259831926005522016995889313462695600644950245628) * 10 ^ 70 + 5514421947842583811346138518958037190676362541729113389281710740110925) * 10 ^ 70 + 1924947374208946502823501119325114111343424616283662485564111476149443) * 10 ^ 70 + 199639273655341360026586345468142498166787209734983400890935673407972) * 10 ^ 70 + 2024603746794692510119126535575983583572669129988994764182275137079666)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_211 :
Polynomial.coeff recurrence5Scalar1Left 211 = ((((20205370726 * 10 ^ 70 + 357027450373992618238647366469506959351490415736321073253563342997831) * 10 ^ 70 + 5361714319159367613775229174173975441377875092962078277269067999613237) * 10 ^ 70 + 3991963775030979278386091215166255791068431803671083399485345325005127) * 10 ^ 70 + 6845043936093718824748291798094797021919591511002032489816460574973899) * 10 ^ 70 + 8120164931255406686162052723732733685602410036776723282377609242998611
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_212 :
Polynomial.coeff recurrence5Scalar1Left 212 = -(((((18881681195 * 10 ^ 70 + 1722080085283005282009205624709317407219802226503730070723896727711525) * 10 ^ 70 + 7964958856548754836007791506784537231356867123517942049304612524934963) * 10 ^ 70 + 2794552725730187969905864831268471935017538114289745147463300812400249) * 10 ^ 70 + 5855700368797556201305170158293476442207490534955519392417591377616782) * 10 ^ 70 + 6219357850565027667395561303986091326768605359689390818332086555513125)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_213 :
Polynomial.coeff recurrence5Scalar1Left 213 = ((((17294522097 * 10 ^ 70 + 5759496915301812417530609101480759876298218925771322282249078116290207) * 10 ^ 70 + 3274168915724157305680410686267435277508953719301380867017867739735249) * 10 ^ 70 + 7854774084361968058954764234486840548489011187362046479936384544136640) * 10 ^ 70 + 9822629436622569216343062112717215659162551298644391140206686380978866) * 10 ^ 70 + 7769965046191021843342747234624107748263832073249409898695449776159906
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_214 :
Polynomial.coeff recurrence5Scalar1Left 214 = -(((((15517805932 * 10 ^ 70 + 7457688403666448188637272821491791893708774112677580519471599864975659) * 10 ^ 70 + 6066733270862857780069737316213139125848772943012393794104084682368095) * 10 ^ 70 + 3608374215960965898238265259719040096101403899400645462208195838387652) * 10 ^ 70 + 4277711820798194524886063188404518015272353651624997740421256958161324) * 10 ^ 70 + 4264503406853231979939155212994775781847275131982562820276132082646061)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_215 :
Polynomial.coeff recurrence5Scalar1Left 215 = ((((13630438083 * 10 ^ 70 + 949276178227424082627634799111686205747105719042109275034136728088166) * 10 ^ 70 + 5856699669882939773048688327383287669273688117816708783030710538416175) * 10 ^ 70 + 7925270567011975198512185974047723782155612232072055396876358024683713) * 10 ^ 70 + 8473162345167222916815073336470152173343528648136929571574675501437426) * 10 ^ 70 + 6406924209802656608087245435102824691989702262262072816931079892502386
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_216 :
Polynomial.coeff recurrence5Scalar1Left 216 = -(((((11710548385 * 10 ^ 70 + 3658077047365930064872827670154717756406746346543067513500506025647655) * 10 ^ 70 + 75093149131475305366100530928058324853302628991824246836619815138097) * 10 ^ 70 + 1844740381739697792526058889166430151997996531833130080954735808845507) * 10 ^ 70 + 6611208242853564692935574857107990823580943240160430635793061650520918) * 10 ^ 70 + 7557391598154973336244016049384345597930185016268861248308869085847790)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_217 :
Polynomial.coeff recurrence5Scalar1Left 217 = ((((9830223211 * 10 ^ 70 + 9688266258502024369788552973456468279503129143532246277172908159199040) * 10 ^ 70 + 8156793668446174150402831653688698789850250690468278976432673179924159) * 10 ^ 70 + 8566359389675192097001063034430438161169534040190118750769404092463666) * 10 ^ 70 + 4493768061578358121674375497327306415194136155203192983561843798849049) * 10 ^ 70 + 5662995157584418677886880654641846246555504380200475771224398459038115
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_218 :
Polynomial.coeff recurrence5Scalar1Left 218 = -(((((8051221786 * 10 ^ 70 + 9481712379328808835967725297265230554147436576524262483804647213290881) * 10 ^ 70 + 9805612114057939541325319804036612541325256989238774642238846179487807) * 10 ^ 70 + 2019184998663205717106120078638943866478148628932177125894274790922879) * 10 ^ 70 + 607421346806586269529064472029096856256983303161138768416791877096962) * 10 ^ 70 + 549260006551320302407274419582591964315302322763763619610381562749374)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_219 :
Polynomial.coeff recurrence5Scalar1Left 219 = ((((6422006151 * 10 ^ 70 + 2049332713148589647440644140509934709576731291144117291992968330983099) * 10 ^ 70 + 1264077722751181858003184066191082080194800854821694984743583234354218) * 10 ^ 70 + 7902523939399608615418072339789560202596882893197006380549925449203392) * 10 ^ 70 + 7990187936741601009490918879899992636875033636335898929853917244265434) * 10 ^ 70 + 5517757556982167910271998666284978355012285645369731371441761720344756
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_220 :
Polynomial.coeff recurrence5Scalar1Left 220 = -(((((4976231616 * 10 ^ 70 + 6641789918333244158588941607382349748543784833171151163610247232365763) * 10 ^ 70 + 5374374691469292578780643568543456130963334998641366923884464959509456) * 10 ^ 70 + 3748331796959868312287485679390801048044536723326168024532163487035731) * 10 ^ 70 + 5437639116464986244106662861783164098350825894735483601105635839319727) * 10 ^ 70 + 6376011116889451276317659564772705034793898181021419675244957143495894)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_221 :
Polynomial.coeff recurrence5Scalar1Left 221 = ((((3732662665 * 10 ^ 70 + 9717412388835706624024766190330828389445053517965929622488902514441154) * 10 ^ 70 + 3892029122167822169141700496712129321225773018786640847955546220061869) * 10 ^ 70 + 6474801047434676022986802303766319397260368215694487326070187867367492) * 10 ^ 70 + 1528481690877186491924060311653052104943202772358945381886730277963984) * 10 ^ 70 + 6529604913065745525615395030338536073507043823880055470104728994754274
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1Left_coeff_222 :
Polynomial.coeff recurrence5Scalar1Left 222 = -(((((2696323878 * 10 ^ 70 + 857603042550544811749488628655515456194835922758051207803597703021292) * 10 ^ 70 + 3227305320129384222263081392166742282960388690528363347959069505383255) * 10 ^ 70 + 355218243979690683725095891601160508921057564529319366267916273372569) * 10 ^ 70 + 4620053960508002371752460426739924925985076233314308661468689304078769) * 10 ^ 70 + 3880737474691090819110195081632494068705521873716784247649798032114285)