Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar1FirstPart0.Coefficients159To190

Recurrence 5 lookup certificate: Scalar1First 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.recurrence5Scalar1First_coeff_159 :
Polynomial.coeff recurrence5Scalar1First 159 = ((((5 * 10 ^ 70 + 9607939367946331642192200163366066075376757434164556092373100499801419) * 10 ^ 70 + 3477293959570038371084707455569157582972011096168082446433012649023714) * 10 ^ 70 + 5665471156383416329828731086616865402021886300299364609483451010630502) * 10 ^ 70 + 9525501573388325237595632239987867008836229294378215314447814762257) * 10 ^ 70 + 2245146419012221464653229454837455973318717872714603666108574522337672
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_160 :
Polynomial.coeff recurrence5Scalar1First 160 = -(((((14 * 10 ^ 70 + 861247955897046877455419930664509292237301861128548037740368662940044) * 10 ^ 70 + 939628854994825288298995333606105027126130014954386019516596383124081) * 10 ^ 70 + 1870186190812245153655368424517483137251647275788452082162804567749742) * 10 ^ 70 + 1879076901019900675182066840223134120849830589144313975771911772272965) * 10 ^ 70 + 2157240041892452977564877322308144001348062617392849183273226716731418)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_161 :
Polynomial.coeff recurrence5Scalar1First 161 = ((((32 * 10 ^ 70 + 6827284871297612203907957185646794899146376012015406725072825939732574) * 10 ^ 70 + 3006336149687421546852898686305380674883778029101359217299553261862148) * 10 ^ 70 + 3896325427084349617971707180759782340167382617484950125905000399725324) * 10 ^ 70 + 1438043127592611772006845477852785176882912383846709818606952839679603) * 10 ^ 70 + 4219509622513365507514853535869373129620770378556565748204891768954655
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_162 :
Polynomial.coeff recurrence5Scalar1First 162 = -(((((74 * 10 ^ 70 + 4578858682342250814600017627085549910697014086998182000842996930979927) * 10 ^ 70 + 3974210279612068503917952885231856106430077003227760237156667837734085) * 10 ^ 70 + 1873233435655353543176972187041444535131419221928769872136552426146207) * 10 ^ 70 + 5858734948553910424710288926655843888437881467154788290205353884960444) * 10 ^ 70 + 6186696735956803620406229360694233280303095195048624325745634182875089)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_163 :
Polynomial.coeff recurrence5Scalar1First 163 = ((((166 * 10 ^ 70 + 5689120295750373261010188321451625827487352281070481989762298057976552) * 10 ^ 70 + 1354078684430046331114877365947801376282889618759433217572243755340525) * 10 ^ 70 + 3916180307711316213200392868278590467746853089059120378438041023514732) * 10 ^ 70 + 9413695810080050138982594983445692306207966028518486388569949552071741) * 10 ^ 70 + 317786917261475139357558050818761121551533421520600009026515605579631
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_164 :
Polynomial.coeff recurrence5Scalar1First 164 = -(((((365 * 10 ^ 70 + 9251410512084707464159634831307932686859265129787246450381947908539004) * 10 ^ 70 + 7978001434514080721223988068280416851587955731519632810455510609123040) * 10 ^ 70 + 6443024978879020800288016212385253195356495862852080987176420677804078) * 10 ^ 70 + 936513397049311343803045561556691579885375959531611922116124422201388) * 10 ^ 70 + 3285537150050755787989491674809277189920086699973707885500494640310832)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_165 :
Polynomial.coeff recurrence5Scalar1First 165 = ((((789 * 10 ^ 70 + 4575136560907869392820858019814048136235503589274450901984076308467950) * 10 ^ 70 + 3617411486566632396303875342480386959395068463254094209521330261247209) * 10 ^ 70 + 7656299534351489422216268727080074531722197886630041194212916967405685) * 10 ^ 70 + 3072598566343715249172642008915228703492272672249044820347858332958988) * 10 ^ 70 + 2439400206321785660902076252560197677764428213535809168044255888330497
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_166 :
Polynomial.coeff recurrence5Scalar1First 166 = -(((((1672 * 10 ^ 70 + 7291000314921580928528870691479127785332174310215181223712315502779159) * 10 ^ 70 + 509877680424287040212017573851423819860886003832429802861699193398502) * 10 ^ 70 + 906785796578329431091748037775026338949928600207706259212593825957269) * 10 ^ 70 + 3562081139034302134631416408331655045433068478663536969819085594336556) * 10 ^ 70 + 4091933050341154846211850442009845021547554749970809288482533345926977)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_167 :
Polynomial.coeff recurrence5Scalar1First 167 = ((((3480 * 10 ^ 70 + 9988071801944780218699557652908030323984105665055333933748130970914813) * 10 ^ 70 + 8628567190511288819015087161677402313579691760514437254078679430377200) * 10 ^ 70 + 5838220932195149812832687079513794029677143487506230215319247016716440) * 10 ^ 70 + 1342414232885174717695127993192340353774128096504685527971208100367288) * 10 ^ 70 + 6118532769969056194275464761118169484942241519937788894511348926556456
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_168 :
Polynomial.coeff recurrence5Scalar1First 168 = -(((((7115 * 10 ^ 70 + 1419588099408554119007077596218452862376910211929796387707002743446809) * 10 ^ 70 + 4430383005890541551142308936457690660506776975160944725805773602080234) * 10 ^ 70 + 3325969589374310154392926619302803689547441714044362289351158728983337) * 10 ^ 70 + 6154786291763043510319597648228268127868499065075957687858135329936300) * 10 ^ 70 + 9117822861577423887770289143463289194295926177037090792386630732916361)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_169 :
Polynomial.coeff recurrence5Scalar1First 169 = ((((14285 * 10 ^ 70 + 1119681948198329608574338440620490127591340219496101563628273074983833) * 10 ^ 70 + 3075584592287473309894159682742152379734571796973608266628968184909006) * 10 ^ 70 + 7345755287492052003898858811229518165232446146855809182060710418318840) * 10 ^ 70 + 877411876947166321493075150951846486867746263450409371704980967622207) * 10 ^ 70 + 8547260055421104088451076439550021395743630387635788782542625172107208
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_170 :
Polynomial.coeff recurrence5Scalar1First 170 = -(((((28172 * 10 ^ 70 + 2789110433875337721236398094779166753201200226785918606490384012154734) * 10 ^ 70 + 9196324729497086918511378712771921280293199189203646343715802559300068) * 10 ^ 70 + 383926119811352539137356335843319807405114310776291290829523297189937) * 10 ^ 70 + 4212212341963386295645151721540995068940792955260733100760718430455323) * 10 ^ 70 + 4217765069807526275987163194407810504803134775464049523425251920349516)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_171 :
Polynomial.coeff recurrence5Scalar1First 171 = ((((54577 * 10 ^ 70 + 7116745155057686557354988323358880560270322986845846404382959145802397) * 10 ^ 70 + 5314751331554255286593874610927022334492853563579640158185382747135348) * 10 ^ 70 + 1096947366805672380774979500519968936057012193205941458758306254989843) * 10 ^ 70 + 7380335674704694050004208675232673690642232570404115368581350931866800) * 10 ^ 70 + 4707454650883082816997459965823268787435607230576211612747704570454754
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_172 :
Polynomial.coeff recurrence5Scalar1First 172 = -(((((103867 * 10 ^ 70 + 4120444406562898943513805092639948446924475869618562646864746484283642) * 10 ^ 70 + 2047547742971358141556015887285109093646693998729906747488323908041908) * 10 ^ 70 + 1531609576237301013789912259669821490635013842687326777917639246885637) * 10 ^ 70 + 7685780883208125272645036567324805822226723897063000124207273918038081) * 10 ^ 70 + 5936342580981876337799580647464805397185082547569413419458997489611646)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_173 :
Polynomial.coeff recurrence5Scalar1First 173 = ((((194190 * 10 ^ 70 + 6956497336885437109804888986834872975608867979661648011465398526657249) * 10 ^ 70 + 1474567923994745098653193570420306313847076706693175590877484753279076) * 10 ^ 70 + 4697324495328301065027326790959958390951816063045400086087375929656242) * 10 ^ 70 + 3288645981644600486375050609373145967369134520032774367818172576977064) * 10 ^ 70 + 7807417045885653112587096268804392646128094589566145179015758584436158
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_174 :
Polynomial.coeff recurrence5Scalar1First 174 = -(((((356677 * 10 ^ 70 + 6720181310788818636164883580741500865602569401646915617236523373220371) * 10 ^ 70 + 5150479657800583276851428235323812430990994219931693840344089612590148) * 10 ^ 70 + 9849612104309682906948644540002601095473775406682178350898528979607143) * 10 ^ 70 + 824404965986112801502296246361326532228273948460471383177897594024591) * 10 ^ 70 + 2753363427461576572186328117835663780958866194079180780189873537103470)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_175 :
Polynomial.coeff recurrence5Scalar1First 175 = ((((643626 * 10 ^ 70 + 4405252563387595225879375568333502183629957064236549100788037970406482) * 10 ^ 70 + 4807970598343463767495323443498557691383512468034674955009522038057603) * 10 ^ 70 + 8193770626183176430143664665215546418588446435468641582631987713585996) * 10 ^ 70 + 2243157672568067539249618740536212800902223396119234809575153123879997) * 10 ^ 70 + 2800006587151820685218805700830132704255603858190506438032553685046460
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_176 :
Polynomial.coeff recurrence5Scalar1First 176 = -(((((1141071 * 10 ^ 70 + 9963879016043586952297679054487825057452021547135592844256805773873960) * 10 ^ 70 + 5832412705092035735184218799709688326231142882611960423727524227548631) * 10 ^ 70 + 7699985542605021673389082861635931440573965541171971314935609451115034) * 10 ^ 70 + 9022502008654273461571885028221095593114566897777813787335063819543216) * 10 ^ 70 + 7809909956955450272776390360452296649559410020781548554859664793460935)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_177 :
Polynomial.coeff recurrence5Scalar1First 177 = ((((1987572 * 10 ^ 70 + 79069250075935838566743558660153485895605466244011510780727291085377) * 10 ^ 70 + 1099785981834094751602274420087570593677556787611922625825919489666288) * 10 ^ 70 + 1733709634448640216806558112314854738219067446784061810269151915508685) * 10 ^ 70 + 5784066096170047786502402537260719392269903053388411897756368947068421) * 10 ^ 70 + 6067330471255648841824098538635417038213532203665476844216451088878747
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_178 :
Polynomial.coeff recurrence5Scalar1First 178 = -(((((3401507 * 10 ^ 70 + 1891410460175264069962472774757350575020054096897533063063397533511055) * 10 ^ 70 + 2814320875834070836729963039503426345916485500244130609780315745801744) * 10 ^ 70 + 5152648645544270249190518354126405590358749901362772652829821062393348) * 10 ^ 70 + 1571541965518107188901413117610456093632385951494349867766136715878571) * 10 ^ 70 + 72078585930097268643494008307884055282621582553610522667315994656438)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_179 :
Polynomial.coeff recurrence5Scalar1First 179 = ((((5719593 * 10 ^ 70 + 8403575633258796093609858493062349573905125995479759920322366730422632) * 10 ^ 70 + 4326315112894192784069075654841337338551411597274859808266110189409567) * 10 ^ 70 + 9836848924220602484929611929351616489865585230438691160431264092976931) * 10 ^ 70 + 9527785323224026784370836633689575266871413128191067129265461220011958) * 10 ^ 70 + 4689000237405439572631818086634619464779223004396939963545325902393886
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_180 :
Polynomial.coeff recurrence5Scalar1First 180 = -(((((9449510 * 10 ^ 70 + 900172527489708026004815896041357311088760583710955073949206016364913) * 10 ^ 70 + 5519239152541578843538284521718270454938594009327262645572019378302144) * 10 ^ 70 + 4322860413917477986914342635929457706165269751700044192737410657318643) * 10 ^ 70 + 6450621740364605399764236946619020148511059124324320852169666501849381) * 10 ^ 70 + 6863224410151704775537796628033350696417813425392973731720621180579239)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_181 :
Polynomial.coeff recurrence5Scalar1First 181 = ((((15339354 * 10 ^ 70 + 8629859065297105430047867654055718984473561494131507418683020641146346) * 10 ^ 70 + 3885474799670841933740252908345828167691965451997345729564348975937189) * 10 ^ 70 + 4886223243474051803405561237665300829237303074824526006959949712764272) * 10 ^ 70 + 4823741848913583901225279006935853142852613260262463518866426601765542) * 10 ^ 70 + 8347583796630659968060200704746900913042050292397802793316643529550781
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_182 :
Polynomial.coeff recurrence5Scalar1First 182 = -(((((24465846 * 10 ^ 70 + 143661166661881462742739735470623645902945018991184151100915646243973) * 10 ^ 70 + 877466286204010268880912250651544869812946088508905075364570516891803) * 10 ^ 70 + 6909152159564291756874560294663333289891791881967279809521969103741305) * 10 ^ 70 + 2218186279521929619598687409954039280415518029070811593850519524811062) * 10 ^ 70 + 3154151117121354147644364151668897910233449317871130186164112372090824)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_183 :
Polynomial.coeff recurrence5Scalar1First 183 = ((((38341446 * 10 ^ 70 + 6684298410637106504433657955684219505631897031048355318613076616479001) * 10 ^ 70 + 7958548951768093275784194289044851249953213137975371910193161519680890) * 10 ^ 70 + 9975612970108164720316813766387838097105982424346682522417378287548930) * 10 ^ 70 + 6223675477703434376423840759417626005916026871725570348372775277695225) * 10 ^ 70 + 9734476175008915156820825826397644620502588794302528037468866595831340
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_184 :
Polynomial.coeff recurrence5Scalar1First 184 = -(((((59037726 * 10 ^ 70 + 3929354769679135000495903266971851780319752308590869311434851404162077) * 10 ^ 70 + 1032807139580163768793647006077127102011999674748756394927554261913783) * 10 ^ 70 + 2810285267242336171043776837934432345837752658051214436730605102426063) * 10 ^ 70 + 202123608255487985933189278201123091750720691622902904588366662655479) * 10 ^ 70 + 9132696573637205233243289354498495864730488240184955870480785332152605)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_185 :
Polynomial.coeff recurrence5Scalar1First 185 = ((((89318043 * 10 ^ 70 + 6485639699531540085868660467770835226631880078228231164469298822545867) * 10 ^ 70 + 7820024745341771758597440633631391378903883234714251157879642544694675) * 10 ^ 70 + 1206906833692437942286900062916445812925281540292534564096071499850626) * 10 ^ 70 + 3660961694696466333016619034664579204898111657117945074549593815185011) * 10 ^ 70 + 214619152893635902344184151175097873779662354478105134730263710886162
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_186 :
Polynomial.coeff recurrence5Scalar1First 186 = -(((((132767090 * 10 ^ 70 + 1736790310364512150864722450470506106561679799362506704831251355852444) * 10 ^ 70 + 9177478177691808252240034730995321455288266616104781368196014154047098) * 10 ^ 70 + 5170359853431304554880005245736673267424975847491329799560745900417583) * 10 ^ 70 + 7406917030371623482641401220669113893731262308690708962086960423923667) * 10 ^ 70 + 3399755277525837450711206717393190887043074398115032959222048533551765)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_187 :
Polynomial.coeff recurrence5Scalar1First 187 = ((((193898274 * 10 ^ 70 + 3488750761240401601336934392272897668034697482639256377397364323352730) * 10 ^ 70 + 1080494513619063486195874546116985931881569429871111642148605720441172) * 10 ^ 70 + 2460850699934371267711893048376730368726414873128172755028566799994499) * 10 ^ 70 + 4960412908823321585263221965647300916586106839118755127289529296429311) * 10 ^ 70 + 6892785634363702916106704256720438599469452118984264757053913613922782
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_188 :
Polynomial.coeff recurrence5Scalar1First 188 = -(((((278213043 * 10 ^ 70 + 3763893541498054538363193074134020831586601466652365791062750236181341) * 10 ^ 70 + 9563633495613862795644943123984245322187773075825309339696879411982868) * 10 ^ 70 + 4161203103924835652831366587678027008710782360278506617277627080942635) * 10 ^ 70 + 2611348089323338976269954916425608223251014125346127925656008843238093) * 10 ^ 70 + 4867617793508410036419771964867866850828538034915851217341137939338639)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_189 :
Polynomial.coeff recurrence5Scalar1First 189 = ((((392180211 * 10 ^ 70 + 9012554066037258678361407920489217115613377045120160862491066391766666) * 10 ^ 70 + 7940391593752655870576401644926199924099061506140289609225357943895057) * 10 ^ 70 + 5055666928999757907436699254674361029199141988471964769981109217921271) * 10 ^ 70 + 9349491528900430178813431573232077194707757977103542095610525409355606) * 10 ^ 70 + 1645357373757450880697617554712345799255592068935491884471334284134125
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar1First_coeff_190 :
Polynomial.coeff recurrence5Scalar1First 190 = -(((((543099765 * 10 ^ 70 + 4040147206785307909610482410880550403800342860727060242831941588802468) * 10 ^ 70 + 3320257616546746972120026005410316354598831895458359322829953860018761) * 10 ^ 70 + 9862946553613731865791944720347331829047413697575626445152095919996541) * 10 ^ 70 + 3797714244817386937033052789748738175996109944437711702599664367277172) * 10 ^ 70 + 1762703277554183004221968110231723238032390495649190117635552595917259)