Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence5LookupScalar0MainPart1.Coefficients222To251

Recurrence 5 lookup certificate: Scalar0Main 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.recurrence5Scalar0Main_coeff_222 :
Polynomial.coeff recurrence5Scalar0Main 222 = -(((((30844441961 * 10 ^ 70 + 3702612428305070532498259269844984511670061521240956827489598160312699) * 10 ^ 70 + 4412083180489522337679868854540200853115894733976904793593289512657333) * 10 ^ 70 + 5830330009493478249618700961352748017943048540811138040613030430195485) * 10 ^ 70 + 2679016155210242535151535122963634772683601356606702198770863974075000) * 10 ^ 70 + 5143935265706898155230597189749029861402345315793913250098593092292288)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_223 :
Polynomial.coeff recurrence5Scalar0Main 223 = ((((25744311500 * 10 ^ 70 + 8910056892287104700398464069215547396442995793593877006092702413352796) * 10 ^ 70 + 4483512835124751095381940844719432433918162499023310227814034180364876) * 10 ^ 70 + 3499356070603612809841488471133885955970421696201020237289086761689037) * 10 ^ 70 + 7907123824689660637987285766766429861745960714465038363312507324654086) * 10 ^ 70 + 1099726638990807209406923121957124162589794533375797769372894077433622
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_224 :
Polynomial.coeff recurrence5Scalar0Main 224 = -(((((21133887237 * 10 ^ 70 + 3868118564492008832301375364464639212231361965145042930815592291751606) * 10 ^ 70 + 597810545547422735383163479231444747453587257043825139588522249902232) * 10 ^ 70 + 8183076180631717410303935499085665990729020546267599049413980795860446) * 10 ^ 70 + 2802799064655125579961689683361048119055588487555971798680006085208851) * 10 ^ 70 + 6399870756126828693232313933183624946787431480557017458450700903469157)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_225 :
Polynomial.coeff recurrence5Scalar0Main 225 = ((((17061295305 * 10 ^ 70 + 216439458143337784781464567647225475550111635374108731636690411385728) * 10 ^ 70 + 5373448233196128441095140768009376747472260209339444944865309676670105) * 10 ^ 70 + 9822257430782519162516651962857532760724397540623475583877703784172407) * 10 ^ 70 + 2519608877152993846132450564782610493526491306573984230697294863127301) * 10 ^ 70 + 3209653569100316909794742451556949759419413379358681081662674029535506
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_226 :
Polynomial.coeff recurrence5Scalar0Main 226 = -(((((13542962637 * 10 ^ 70 + 6863477405948706819217582930004556114428514402038859672778164325994255) * 10 ^ 70 + 7279428632162915658517077579735433654363323789010917773226872440158387) * 10 ^ 70 + 6493176876764123214665354950312411590415332455552999532935230050373117) * 10 ^ 70 + 9585154230905816940443786895480416924830470714536506904604485347910772) * 10 ^ 70 + 8011853544885869420166704799602777990256075189838501402375242294612934)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_227 :
Polynomial.coeff recurrence5Scalar0Main 227 = ((((10568500565 * 10 ^ 70 + 7875467465871162422252881216030880445334826475979417003808979157206427) * 10 ^ 70 + 1176019494183676663213449002480725276252443971745080420806748948957543) * 10 ^ 70 + 5510570335681094599570561366270282580530161665018725487626538518521586) * 10 ^ 70 + 5335026147438170183957816636439110201047083183431171179731961925086898) * 10 ^ 70 + 4017482334599262353166332476190611319579394518837104940941114170340145
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_228 :
Polynomial.coeff recurrence5Scalar0Main 228 = -(((((8106536459 * 10 ^ 70 + 1958893905446750309181881203227386400094251156821386941687046291123596) * 10 ^ 70 + 5923603619577431074809358839930244639016688063405545994807277555582967) * 10 ^ 70 + 4916103700215242915940478957015964123889519446007996548073162082122315) * 10 ^ 70 + 3262847676261827452047053464987805519570526503551919389467827289736991) * 10 ^ 70 + 7992411577152313644164025362856142632883303714488990494799083734939243)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_229 :
Polynomial.coeff recurrence5Scalar0Main 229 = ((((6110832019 * 10 ^ 70 + 9908572865423678791835537204995868298887489800487037197402001883829415) * 10 ^ 70 + 8547639465506701382469190420622102695017239930571648054197033874469126) * 10 ^ 70 + 8295923757549549989383763937794367231603476361801529685036859506749490) * 10 ^ 70 + 46719200507837027892350542914592498018520523087966625935617459716110) * 10 ^ 70 + 1009052162223176033584918445136590719301776689464478838125007790495531
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_230 :
Polynomial.coeff recurrence5Scalar0Main 230 = -(((((4526130256 * 10 ^ 70 + 7587224640329205897045989497749103578219851286750625439997049225756264) * 10 ^ 70 + 9928505291822044704940619845774838148580633647712764296447356930693442) * 10 ^ 70 + 2047580808949533331499553048399540250194626773065597557656493015477664) * 10 ^ 70 + 4369249071484652368287752724529980270890523886922214333588973669093944) * 10 ^ 70 + 226453555845174428216727637919866310746748841665694866495314383858623)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_231 :
Polynomial.coeff recurrence5Scalar0Main 231 = ((((3293314711 * 10 ^ 70 + 3940497493298293813281216403514673536922063761425228569391744852659454) * 10 ^ 70 + 9180007024723230090859426009185756433562056704647769143041653758517079) * 10 ^ 70 + 2884512436175012925395853209349600384876096505952735770532564756985478) * 10 ^ 70 + 3904416921173106497909113145732832896447543426249813439801198804564592) * 10 ^ 70 + 3138141178503005557778284990435055520622405995511203497406017935272191
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_232 :
Polynomial.coeff recurrence5Scalar0Main 232 = -(((((2353619657 * 10 ^ 70 + 530507939321283850881764117548582243320128317191319276132408905844221) * 10 ^ 70 + 2322306144865868540222225419489104699212641254165840350717112084459454) * 10 ^ 70 + 1304551978652307114211093067015919604033137969068061489568022141935991) * 10 ^ 70 + 5437454671638196258466650729822243055222537780714806509332034868027285) * 10 ^ 70 + 2943026307089148773930205502369128899860825919142317660139028735089700)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_233 :
Polynomial.coeff recurrence5Scalar0Main 233 = ((((1651777781 * 10 ^ 70 + 322414204544410850468094938207520102442137844633136125470013355422636) * 10 ^ 70 + 6218097276092668062476476788762188914803540884751339553854052861129739) * 10 ^ 70 + 4475191177619810938538901356528606036274388577136143789585701740773244) * 10 ^ 70 + 9659085681702007078834385062216309707479321343698063125531537500986987) * 10 ^ 70 + 2330875023048006599968040116753615758242022852588142027475688402422947
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_234 :
Polynomial.coeff recurrence5Scalar0Main 234 = -(((((1138116984 * 10 ^ 70 + 5646224068116430419135235545314943725858964354412545212078557945977621) * 10 ^ 70 + 9659803686189116414259354004262365971290542067437097136814207093553182) * 10 ^ 70 + 3572820545732378660159940110376662595516002667723908093453816347107332) * 10 ^ 70 + 4825193746739671299661179322029680744181481024698077213435257112930340) * 10 ^ 70 + 4629536178269318888415835882328160411066498625501853392458123128605811)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_235 :
Polynomial.coeff recurrence5Scalar0Main 235 = ((((769711463 * 10 ^ 70 + 6542761724474303339304475988160087100213950498558418570727518680870605) * 10 ^ 70 + 4178586824459689597613337261786696379874248560384933145406899034920044) * 10 ^ 70 + 8523516336079974995702563906784043524114813439973436590909862075846071) * 10 ^ 70 + 8119954225854720744023950503422530990345201944864740984240702824114678) * 10 ^ 70 + 3737991522615172113927686385863282683421914514482566874725379815319874
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_236 :
Polynomial.coeff recurrence5Scalar0Main 236 = -(((((510751345 * 10 ^ 70 + 8399966419058841420348136829675347722900268815669915582209433995589684) * 10 ^ 70 + 2051194038949629231539657033657740981864472368783633923355937606504176) * 10 ^ 70 + 3683332937485811200867039886353035309809057799320175834440011389528801) * 10 ^ 70 + 9518730381182990399869111731209853974935414934715309245646767239827789) * 10 ^ 70 + 7544374496596607329671529018371299754480423305709594500578238643766365)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_237 :
Polynomial.coeff recurrence5Scalar0Main 237 = ((((332321957 * 10 ^ 70 + 9047959110669757004524790263847346118112885584693192268766581965139896) * 10 ^ 70 + 8675523632572625842367140050369256552926430120761495102448141381795550) * 10 ^ 70 + 4245889113527909866475022850403197675467619576316599618155134452622638) * 10 ^ 70 + 7505711313672709706590400753646501677170775107839799017015909550657194) * 10 ^ 70 + 972309438007858171881939957040188455176291409180689356909793794694795
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_238 :
Polynomial.coeff recurrence5Scalar0Main 238 = -(((((211783804 * 10 ^ 70 + 8761856690013745205941970556557218093658256508366985030787548197709854) * 10 ^ 70 + 6756381570560257001815426034254079325644797671344316210143678118769862) * 10 ^ 70 + 8744774244298633740036395456033258056486898566299116987666706068724827) * 10 ^ 70 + 3429422204633670340314387553372335044281557291214160045445154364931134) * 10 ^ 70 + 7338126807220827625786089887086300369575241036698269458866129173313710)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_239 :
Polynomial.coeff recurrence5Scalar0Main 239 = ((((131924857 * 10 ^ 70 + 5286191418324491544650055066091419056065302898447051365768534195506327) * 10 ^ 70 + 3796338542071206846545123383329984401878650709916124637308306235075531) * 10 ^ 70 + 2025310599769279300565311493665749983238885747042145810933133192625586) * 10 ^ 70 + 9935695993542011620151713916928340793387589522230201368313558156890521) * 10 ^ 70 + 6138885670044276736185412115283858749225249230297220220366096026842286
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_240 :
Polynomial.coeff recurrence5Scalar0Main 240 = -(((((80025439 * 10 ^ 70 + 9028985516013163621583423244991144999903127678671125495400205710088747) * 10 ^ 70 + 1003453180944402245352126671158128080663119654305323672405094461711828) * 10 ^ 70 + 2930443879573815285773707210835613388067675531329735113152306436253583) * 10 ^ 70 + 4778581406154531662221227218902699660573282897320264581409969352944102) * 10 ^ 70 + 5150391119675949808286546346730926201125340912850858861420639335124433)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_241 :
Polynomial.coeff recurrence5Scalar0Main 241 = ((((46939815 * 10 ^ 70 + 6971515558350776647671395539772964493330528320491148219146199604921758) * 10 ^ 70 + 7478804606994365603896560654480536572775229455490407224201299394183467) * 10 ^ 70 + 4347565416466829191102943122801832563537920131448372854337099759292827) * 10 ^ 70 + 3642779667602503706400640471052314462809046565294745017198825967884471) * 10 ^ 70 + 1931750697224870901166711274735254316838319978280989944906614410029483
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_242 :
Polynomial.coeff recurrence5Scalar0Main 242 = -(((((26263010 * 10 ^ 70 + 7381676958384572370028496925710143058011112283377265640499660557631750) * 10 ^ 70 + 4545037124476063744333073357782026458096673227365068917342168700104296) * 10 ^ 70 + 572756522158939314237026902542002020774183422068726550847843370259751) * 10 ^ 70 + 5682204444175236065530868947331064746625086251138604492409464658658473) * 10 ^ 70 + 5779480534765809443114077103641806212410372325862003905778732440532277)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_243 :
Polynomial.coeff recurrence5Scalar0Main 243 = ((((13620277 * 10 ^ 70 + 9707329198578833525760789416769819209663745648982502493447044284951983) * 10 ^ 70 + 264180917765857042987987151317156114775435315742152274739653360914763) * 10 ^ 70 + 6985005069831976562637579187402059337394030952923244699807195233081122) * 10 ^ 70 + 5805908799559402351624201631297786614384574864565250050449883736453854) * 10 ^ 70 + 2850630672332368726792478944440010098481955181162458394994944415035533
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_244 :
Polynomial.coeff recurrence5Scalar0Main 244 = -(((((6092011 * 10 ^ 70 + 8184072620806129454505185897241693752690697132564100706405001473565397) * 10 ^ 70 + 3387325213747148170661117585642893753051852573376376572949375976594926) * 10 ^ 70 + 8681643845621860046277175582980009771818621295761713303750823984655650) * 10 ^ 70 + 2855302544639266827406475588168938163031695030591727236248884694189935) * 10 ^ 70 + 8190169821581160115792827216599429747950156452002842597368191440757597)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_245 :
Polynomial.coeff recurrence5Scalar0Main 245 = ((((1769494 * 10 ^ 70 + 2995514041539931503190781810112205465657074560177283620124398990090569) * 10 ^ 70 + 2196874620723535832966070942062002342444884926479956952697512849890444) * 10 ^ 70 + 7175287922790255567840944829797167557415902573111553782361125523693688) * 10 ^ 70 + 3284396696220879411394496713021447747879087257107607080362186568119997) * 10 ^ 70 + 3103716081433698596444766842761900793667513433194090538304887759697814
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_246 :
Polynomial.coeff recurrence5Scalar0Main 246 = ((((573838 * 10 ^ 70 + 3731126455509939359368264229895426326339587196144879866457001842668015) * 10 ^ 70 + 8906444468831027961010428719169606542246998786098382547607641229831612) * 10 ^ 70 + 3206177538858944097695096492704771559172382756475467445491625525812285) * 10 ^ 70 + 2116753956209984967240025722371702841224368021127618487835809123125081) * 10 ^ 70 + 3574333259482583797284663800802945852270379738284149725884100186936145
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_247 :
Polynomial.coeff recurrence5Scalar0Main 247 = -(((((1716011 * 10 ^ 70 + 185272408295949573212240991853889826894750216287009507376247695385209) * 10 ^ 70 + 8775626718744429505138877414582404044949097160056826193701229788108336) * 10 ^ 70 + 5865769634458985586374927302439240578347096083468039231750387159903495) * 10 ^ 70 + 3952696152873103402848297506877640097560573768261368459994637855004575) * 10 ^ 70 + 2502034317814022041511288458236637405899051435944039852865104010733468)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_248 :
Polynomial.coeff recurrence5Scalar0Main 248 = ((((2146337 * 10 ^ 70 + 1083285880874506211424847593089460142041429870449762323453563501940402) * 10 ^ 70 + 2559007125639825945326570871933454979437208698760519427285571478776682) * 10 ^ 70 + 5534859620836955036630700343595261543724086726559546595798136454490440) * 10 ^ 70 + 7623490867584250788198687369795857218707686505840285991049592017963268) * 10 ^ 70 + 7123420033845835687996588201861638515040517654796544589969780020218701
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_249 :
Polynomial.coeff recurrence5Scalar0Main 249 = -(((((2171009 * 10 ^ 70 + 7399613232637162848827089745923294065808071545967411797769591688415208) * 10 ^ 70 + 5392703280306040360383389902471962738186014203817972083719586591665720) * 10 ^ 70 + 1736425891118532711157308343455080408153042912986406194455773723497340) * 10 ^ 70 + 4092464824404825003227662615352294666898913346224282951830776464215791) * 10 ^ 70 + 2038346013336126982612716896340812316729125587358228693999101293625551)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_250 :
Polynomial.coeff recurrence5Scalar0Main 250 = ((((1980787 * 10 ^ 70 + 9668305277033666330788785515140625163980194204308420246008299898285444) * 10 ^ 70 + 8305108354502962958876659749797562398439736771562910734251865415684451) * 10 ^ 70 + 7306449160170244241861365877397909197632178376395131988654822066889949) * 10 ^ 70 + 7863688286339559131630096134994721999171035485939483400026765272422234) * 10 ^ 70 + 4754591585381314196865227535443186101368425691108037503887505690697341
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence5Scalar0Main_coeff_251 :
Polynomial.coeff recurrence5Scalar0Main 251 = -(((((1693427 * 10 ^ 70 + 3882830399453670629041245591675802490815520301999694850942027585162909) * 10 ^ 70 + 2364302444060842631219168302398573189191048735317528141882931502463326) * 10 ^ 70 + 7937587103447162777393172629125514445941067472666162439877920391080203) * 10 ^ 70 + 35715429536617740646350756132702912933871647472397587623164967892175) * 10 ^ 70 + 1698161538507898280342632859687017783653670618397173249300343986594818)