Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar2FirstPart2.Coefficients302To328

Recurrence 4 lookup certificate: Scalar2First 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.recurrence4Scalar2First_coeff_302 :

Polynomial.coeff recurrence4Scalar2First 302 = (((2350978343293408902296 * 10 ^ 70 + 7163060501467373884676347968970682674660052954119809068814467580772260) * 10 ^ 70 + 4950806937452944378627758335956572872439535482241189462026751273038912) * 10 ^ 70 + 894596023779738591297861204567308654038324143865498455605342054129033) * 10 ^ 70 + 2861332333903759709682256132750388855848419607738096334084413446727645

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

Polynomial.coeff recurrence4Scalar2First 303 = -((((1142445933958270856080 * 10 ^ 70 + 6189117464907327396474437662638815873402024824106559378994512589369965) * 10 ^ 70 + 6716244149757620813264487749522673122218809068434011599324123940172232) * 10 ^ 70 + 1225650972587925838756062511928115268527448715847643389234094758940984) * 10 ^ 70 + 4193012967631853103430248890338698232284665699600919872320575530088266)

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

Polynomial.coeff recurrence4Scalar2First 304 = (((513257842877035667169 * 10 ^ 70 + 5116332066180545693473164763988234349189493144626860526216856558124411) * 10 ^ 70 + 9191505994385226949299197026915149402637291903002707611206527622120133) * 10 ^ 70 + 9931851593348198742090231656623470215744386433383503362645072258637218) * 10 ^ 70 + 155249839025789618370072573761645714007452441936354447344173965417815

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

Polynomial.coeff recurrence4Scalar2First 305 = -((((202432317926400756013 * 10 ^ 70 + 1268296256813452016722577912520966998692052550820021215699134375910898) * 10 ^ 70 + 310396166259748148197511680477503439731382590736878045382361997515836) * 10 ^ 70 + 2471246800982139761041442919583500357936532674109132164158182309476228) * 10 ^ 70 + 3308876753659305524457653658900141048279376053573101496489600562623912)

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

Polynomial.coeff recurrence4Scalar2First 306 = (((59545950052908872125 * 10 ^ 70 + 6188488877064029856414702659063856319890881313232066908408625219022113) * 10 ^ 70 + 8963275732120557441254501101358403425836710963719054572125089470252908) * 10 ^ 70 + 3127146222733715329358285154855839176917551379940273215330812012021387) * 10 ^ 70 + 3661863800822207912798334676162869162364356870506046308354148725453141

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

Polynomial.coeff recurrence4Scalar2First 307 = -((((918872566419590201 * 10 ^ 70 + 6257421017316979899330844670887879514005137994218459007664998587151429) * 10 ^ 70 + 4400435268018476296104487361836897491769113821091940435812546776764251) * 10 ^ 70 + 5545524385932345067341733535721696051010697309014796510670596941075357) * 10 ^ 70 + 3282987188148124616950899586831788131336940176365903754636404488860275)

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

Polynomial.coeff recurrence4Scalar2First 308 = -((((18163917094428496012 * 10 ^ 70 + 5554579324897153825661062214191793880506950778505202422884864661434277) * 10 ^ 70 + 4563475499125782668286855104030010920123046027343403224664242304658665) * 10 ^ 70 + 1230408942281665546379347043145332587866001738432048507300400368243444) * 10 ^ 70 + 970288347573825805510433011041466253752996505579393980351535070784930)

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

Polynomial.coeff recurrence4Scalar2First 309 = (((20470094292645426314 * 10 ^ 70 + 3901815900904452186138061772462989759080370668412352188427135074507216) * 10 ^ 70 + 62677902969095992032604638251047752658735402835473258502991450968853) * 10 ^ 70 + 6966439460178583492080155625035918138293293511298620892731800682421144) * 10 ^ 70 + 2108272522069941916941849345707861459931277801307709583828652800043671

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

Polynomial.coeff recurrence4Scalar2First 310 = -((((16888889723697081027 * 10 ^ 70 + 5519423857492563217287579025222216544259353855963105621497452388587543) * 10 ^ 70 + 3452877782694317978455362163226640552867134059011293141195095318765364) * 10 ^ 70 + 2228849650489787615071859479449964984591221840223288144349374254224902) * 10 ^ 70 + 3472380008907804625612666990501585808180378895033817700095681236792687)

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

Polynomial.coeff recurrence4Scalar2First 311 = (((12175168216780580082 * 10 ^ 70 + 7735052475375846848082053269772873398716941647172002690693294016802110) * 10 ^ 70 + 60548593976345109742375328250887694236513533312386660294216915681944) * 10 ^ 70 + 8518585240903512282339098451346565936847761413448978343096549522410792) * 10 ^ 70 + 3299629090701935298037545094063041412226022766044300528658757293064812

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

Polynomial.coeff recurrence4Scalar2First 312 = -((((8098143510143236684 * 10 ^ 70 + 8055840793919836154445646217815034629562610609510234212389316809357907) * 10 ^ 70 + 7914938651684249482273063947582934467915648728903257245833558909907031) * 10 ^ 70 + 9911996994905186649353123174817590950434037506542993558143264393238467) * 10 ^ 70 + 3206753206571144868466872498849312856774012924364887256399539600408941)

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

Polynomial.coeff recurrence4Scalar2First 313 = (((5089910867474364990 * 10 ^ 70 + 5958993229029433504712860778693664250830574097421726727796508882702018) * 10 ^ 70 + 702469414396354375558201316491003897047941727526738805149179111356111) * 10 ^ 70 + 612399222333256161029809408980566833754241737177893533107215260573602) * 10 ^ 70 + 16663649130031015753005377266830233171205456675176556419881083968583

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

Polynomial.coeff recurrence4Scalar2First 314 = -((((3061016630163676945 * 10 ^ 70 + 6323744787306049395997734615059879128942193621677252199730014036861232) * 10 ^ 70 + 7750302883643697325871364152096307436905355418590636286888252400795970) * 10 ^ 70 + 385507372902447655787983649318208583934310755747992944421519099716440) * 10 ^ 70 + 4078539531312252468849473459427664676259452939654329796143731181015021)

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

Polynomial.coeff recurrence4Scalar2First 315 = (((1774040278527762005 * 10 ^ 70 + 292318901181587883851879098927579324341860201964239288604515350058777) * 10 ^ 70 + 5211586592983144173276340280996551099907607760428291578135902095277738) * 10 ^ 70 + 8313382364787040094594529424194805787432850385129402814562844018316874) * 10 ^ 70 + 7638375202161871710010947221637019081628489480757983650312684542406562

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

Polynomial.coeff recurrence4Scalar2First 316 = -((((995115844259452310 * 10 ^ 70 + 5661644728926828482527323196400277508459047395278126501995212677982428) * 10 ^ 70 + 9856195254095109285600271049617787676644763817025741964474431158432181) * 10 ^ 70 + 9234531170326314234032738841914581746771639463040832993902769436871876) * 10 ^ 70 + 2465935207341608233172134466723801721628067849554556159780500457204218)

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

Polynomial.coeff recurrence4Scalar2First 317 = (((541642068458239220 * 10 ^ 70 + 6421351687260349497718295915418039028318658498777710162511897149468522) * 10 ^ 70 + 4346553112788279220203100304780687694471384015436694562606641836443757) * 10 ^ 70 + 434344717923347784931325824036924734414640673335764747607697885600532) * 10 ^ 70 + 4646708304203300676387846411567552724929279031570201740855459997473192

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

Polynomial.coeff recurrence4Scalar2First 318 = -((((286471377129265032 * 10 ^ 70 + 232206181320273295885859723497760320439783158904899453961232627744390) * 10 ^ 70 + 4218283091504140010376187929121870211842254082640263558792290240122494) * 10 ^ 70 + 602326130990485902307349829943443883189666056446954676348079013125777) * 10 ^ 70 + 543611629966592362910480495935216025157407742955420862299655000767277)

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

Polynomial.coeff recurrence4Scalar2First 319 = (((147292756183363980 * 10 ^ 70 + 4160840229423160112691425548338441018038695294080599370871497031185115) * 10 ^ 70 + 9235743449153701602191340192580183420142632515001930807406207448716202) * 10 ^ 70 + 4894639041699539348210191129840045187098083022490561590658269737315904) * 10 ^ 70 + 7761627147008659210908805553878846132150657902327603711768984909725967

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

Polynomial.coeff recurrence4Scalar2First 320 = -((((73595646832986639 * 10 ^ 70 + 4968378449120169232205436158248773434206101122911373597626612233759666) * 10 ^ 70 + 2170680552492845061597077605670722342417957881756031024032178431023023) * 10 ^ 70 + 2061653890298502585035342956696927048163833660292897454853800129896979) * 10 ^ 70 + 1471106043105545077373134575464770955045044515360392059394857950888034)

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

Polynomial.coeff recurrence4Scalar2First 321 = (((35690116032128885 * 10 ^ 70 + 6100482838622274617228250295545411171833998863351046010374788135947669) * 10 ^ 70 + 81378780728721565767407331721448555331682567773363263758275437477875) * 10 ^ 70 + 4736992923196106674246201944491895138069995765591901742942028919272034) * 10 ^ 70 + 1438664849704082717296151665494177975561181794377299310389192438062510

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

Polynomial.coeff recurrence4Scalar2First 322 = -((((16758909961233988 * 10 ^ 70 + 8083155797152062137404676904806035825915845003136868260424420775777413) * 10 ^ 70 + 3299060595133492481778444928075518890217402761104212862918161532475232) * 10 ^ 70 + 1143239597114865140188382256597914484148998092867748496550980057349481) * 10 ^ 70 + 6243394717266348780480073156825985877309461674846334992903459749905450)

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

Polynomial.coeff recurrence4Scalar2First 323 = (((7590028474645244 * 10 ^ 70 + 5842401560757735283608318704991931590274329834939438406064779196257943) * 10 ^ 70 + 5598523689040597603532520589421042428726880074383990437767085926372315) * 10 ^ 70 + 3124587362395922372838943878497303880403997793056708854874827821983759) * 10 ^ 70 + 599683270142624781303789379816956504818557947811030135329307310775676

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

Polynomial.coeff recurrence4Scalar2First 324 = -((((3294208595442310 * 10 ^ 70 + 6650626767543319914813332433382009918120083594600365352352024903828627) * 10 ^ 70 + 2008882877009908301703072640033879554572580232477989781072506156197049) * 10 ^ 70 + 6749002115160206593806290431082509188314930672084114432752761522831558) * 10 ^ 70 + 6837415753679247277208660681406255124433347761515258845791929598203893)

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

Polynomial.coeff recurrence4Scalar2First 325 = (((1355250264614926 * 10 ^ 70 + 9171676662527549037188703825914475563033965774413249824140440181206246) * 10 ^ 70 + 7363702974204881596404829093443682814471891495471679890700512607874969) * 10 ^ 70 + 5999119450111036992751100061974113451031129634957092403026040968119047) * 10 ^ 70 + 9101250934637101406868571182865464068822810616219223756870886990687138

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

Polynomial.coeff recurrence4Scalar2First 326 = -((((517900336187960 * 10 ^ 70 + 8299028799251242138192922196894541449850273339386446838128295897003757) * 10 ^ 70 + 4344334217377342227944820692072927803771592917050179783527916348453975) * 10 ^ 70 + 3901041666324367790701731570963400703960552590876038203720518492916460) * 10 ^ 70 + 5399133221402149833886450763777665794650331478105381894129423030693704)

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

Polynomial.coeff recurrence4Scalar2First 327 = (((175974047097632 * 10 ^ 70 + 2952304925611128469816892395146589670630866594699380824548254488253128) * 10 ^ 70 + 2993990779493950964160392204580526096341882277696477043997726251154582) * 10 ^ 70 + 4091873381778719973733252970290612298510842982979717345454325597672421) * 10 ^ 70 + 3204017272147044116540251669350021242344659562601181983066615068072124

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

Polynomial.coeff recurrence4Scalar2First 328 = -((((46861528527082 * 10 ^ 70 + 2310272360264606598189485857633747428511186194699796993116084888014254) * 10 ^ 70 + 6461238048334946418828369715100379615818238836816898764545498696268354) * 10 ^ 70 + 7260846246878073911081254526291849990267089731148484785489618120404000) * 10 ^ 70 + 3100662265371943511269480198598802123398023738217445796970961392181863)