Recurrence 4 lookup certificate: Scalar1Second 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.recurrence4Scalar1Second_coeff_302 :
Polynomial.coeff recurrence4Scalar1Second 302 = (((3834037411607361091259 * 10 ^ 70 + 3483347502048911596897545389391165745106066620708956628108901761326215) * 10 ^ 70 + 2736009000978119246531569110163676001208840270854743293920879285247678) * 10 ^ 70 + 3834399851674532642888653065796323207997013529381514407905598317429625) * 10 ^ 70 + 1093524819759090280637842384336181954020899220185627495064779542738981
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_303 :
Polynomial.coeff recurrence4Scalar1Second 303 = (((3138279589319785921388 * 10 ^ 70 + 455307676187021995396528383388515203829319748820027324029915247872836) * 10 ^ 70 + 3974601734272882234636784054485433479018139682731213472916267155016791) * 10 ^ 70 + 3566242496770598577001237608585498491289378784029838002244147355943151) * 10 ^ 70 + 5552185259365551714350248660001571287809474387075280943306711057617749
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_304 :
Polynomial.coeff recurrence4Scalar1Second 304 = -((((5264807904993948205421 * 10 ^ 70 + 7271422325869752236914092190760014749128273175423279022405343503019451) * 10 ^ 70 + 1212767991081717566948377102496052370536001030902890076404561899650933) * 10 ^ 70 + 8356677446007604645781195875387697447287142918416907450603834271026868) * 10 ^ 70 + 4554743410838747612131030475375570264926438971469593839583835445267425)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_305 :
Polynomial.coeff recurrence4Scalar1Second 305 = (((5184609788177044872231 * 10 ^ 70 + 8515269466706654492780709085519167243278465629556335267124007116570447) * 10 ^ 70 + 4936554740503091020476521951740745223432501240005833425787821000117789) * 10 ^ 70 + 2756887486442287622417661561595849124100829560103531961039395934226794) * 10 ^ 70 + 3578740685243145178717332070724380615535833841757304450787901610805983
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_306 :
Polynomial.coeff recurrence4Scalar1Second 306 = -((((4279135761154146919908 * 10 ^ 70 + 1073674942477209526077606925332915259407341704061712588720685186363156) * 10 ^ 70 + 3762323291655234075002110225658607861780736437693786361063159262564590) * 10 ^ 70 + 3640209537526864581416712191695232478892088277660603125814694373844098) * 10 ^ 70 + 7553407835710058711467163705503263368811514021667215701123974561418064)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_307 :
Polynomial.coeff recurrence4Scalar1Second 307 = (((3214541556981382236743 * 10 ^ 70 + 5258153026853410625137083280663778992630741912565296357341910895114121) * 10 ^ 70 + 6611880493997961669318681884289229748564962791173991675074064019324085) * 10 ^ 70 + 5695279627197141270119195113870118224195030136420991285322384888945751) * 10 ^ 70 + 2096334217739349808027938845678209620630413648535249705262259907745182
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_308 :
Polynomial.coeff recurrence4Scalar1Second 308 = -((((2270758219878421571440 * 10 ^ 70 + 2288753780267012178205826765843577994827247419824638037426538067120108) * 10 ^ 70 + 2451868124688815719029260693952367317212058302518037908154742142580524) * 10 ^ 70 + 607317997052655950437123660579281131312107064571815448090947875640573) * 10 ^ 70 + 4978355122316906112032164711167179650178807670636740806045800381324942)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_309 :
Polynomial.coeff recurrence4Scalar1Second 309 = (((1533050901045379179631 * 10 ^ 70 + 899481158284711606005910273537271474777822191680510280486984098402253) * 10 ^ 70 + 5481579919061576662510001145934146614001401622822667507362893550147878) * 10 ^ 70 + 3752463868858335134094317034156297487359201697138515851403830452432574) * 10 ^ 70 + 1291796633000815803024380300204707353565259742431341153020253782214659
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_310 :
Polynomial.coeff recurrence4Scalar1Second 310 = -((((998308970396484890582 * 10 ^ 70 + 2865799468707814301753879503088967004765082689485572368757873754602923) * 10 ^ 70 + 3292608785542249217636911459076230380791625506352289567640777099482158) * 10 ^ 70 + 9672190834791528301181922989742387102956765191043589140569561238269703) * 10 ^ 70 + 735608498102295187571806351297206314382471573982906875872189353026096)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_311 :
Polynomial.coeff recurrence4Scalar1Second 311 = (((630584383189671915658 * 10 ^ 70 + 9162439526689545537921900041562238944151383333180343556315727661385648) * 10 ^ 70 + 928646571084137327184866158025116020823432229724734908108434916516154) * 10 ^ 70 + 771293687735790943901037463795649367427855643632724895710582508380103) * 10 ^ 70 + 356398726188656898031454963092641549310126325712061683645872623327178
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_312 :
Polynomial.coeff recurrence4Scalar1Second 312 = -((((387764030062144711012 * 10 ^ 70 + 3765300961213316132428881018363695220361680247655754753856082232605610) * 10 ^ 70 + 4528360925527743166437765802720677435122638464638693935739018157498347) * 10 ^ 70 + 3963599575185433581632282632065178468877351182863830565433797951331318) * 10 ^ 70 + 4127648769916319348828620464100331484213352573804191792609040226676089)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_313 :
Polynomial.coeff recurrence4Scalar1Second 313 = (((232689790114992099143 * 10 ^ 70 + 1621870040727369362880505367647411018323894215343479679443054282259486) * 10 ^ 70 + 3770763426611973010656413078091601772965902123704520301359136682010417) * 10 ^ 70 + 4504485758083579506504389746966464712281004972543506709170436272938532) * 10 ^ 70 + 1982684902583463245333650940372772599939921404082085888774568884787654
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_314 :
Polynomial.coeff recurrence4Scalar1Second 314 = -((((136475838324482626889 * 10 ^ 70 + 6659934573418886476435945707483684818493702177152086758627991056759199) * 10 ^ 70 + 8798833627859750210541059863665392652342022357459769247549289622275760) * 10 ^ 70 + 2444337930136996896765004879385208492324309454947249968624550878054815) * 10 ^ 70 + 7983953768622538815144584941402479358025360345327464678622044971283159)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_315 :
Polynomial.coeff recurrence4Scalar1Second 315 = (((78312773955928452454 * 10 ^ 70 + 9583783364279780059782113332810551126770576779141033124097999428183933) * 10 ^ 70 + 1948763130247773804746746684146709379149820553301202078776252647424140) * 10 ^ 70 + 6142531133529514449026623573703942454133859889293877241095171986683847) * 10 ^ 70 + 8785538243308343802637474818937980022413149312432242118164487411315865
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_316 :
Polynomial.coeff recurrence4Scalar1Second 316 = -((((43989009181657161266 * 10 ^ 70 + 7160111622579197959855306833805319214786916489627594370628487108441912) * 10 ^ 70 + 2439274485126958771592096801876141250007786248565741885044685922753625) * 10 ^ 70 + 878317119491393232097227812149875218757172024411400561959902849917125) * 10 ^ 70 + 4740859971587852327985367817822144238225625638571361198236285724511428)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_317 :
Polynomial.coeff recurrence4Scalar1Second 317 = (((24191746077035536327 * 10 ^ 70 + 4096298773579762199137998469893034973273924757679749842097183773586452) * 10 ^ 70 + 4407355074725207260784382966570220044589091308742966814124049619523268) * 10 ^ 70 + 8575002662050107614996105636849043981352814692231388454574687342103601) * 10 ^ 70 + 3417763504683424237966398736080156893151740295262700430528086456209461
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_318 :
Polynomial.coeff recurrence4Scalar1Second 318 = -((((13023707548663505336 * 10 ^ 70 + 2588891074865954057849178571574352769645220634248500410839604116819032) * 10 ^ 70 + 1012957968562993321773361987303975150959041865920207318887630168630513) * 10 ^ 70 + 2910937249049299033722562375860403264976325052341925433784431582214976) * 10 ^ 70 + 6947602836605387184511601792001317991866750647591832893042605763261005)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_319 :
Polynomial.coeff recurrence4Scalar1Second 319 = (((6860199310039750944 * 10 ^ 70 + 9595855611620893113109764992633792019994788021969487076079504248451091) * 10 ^ 70 + 4488681022144613254762103525707409417780069579225942980281705117115737) * 10 ^ 70 + 3521636851186120058374137351704269799209987188435594317560356174883667) * 10 ^ 70 + 5886224726577122451417815992056254265725894984834950142148681445687169
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_320 :
Polynomial.coeff recurrence4Scalar1Second 320 = -((((3532707886784291354 * 10 ^ 70 + 6964746523916850833068209499673139259148341840774601526996499172921035) * 10 ^ 70 + 1983453882609471331886541912818700715988515913369159519711103756202537) * 10 ^ 70 + 1947638159396404553005981026353712716160930453619510309186156979767219) * 10 ^ 70 + 6933438090815703341099211477098436224321424466777858520102577875012099)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_321 :
Polynomial.coeff recurrence4Scalar1Second 321 = (((1776210168241853911 * 10 ^ 70 + 4129367915385302176946289719489747020001518785612239786779530488463502) * 10 ^ 70 + 7137845035250581598025562050589149544036950544868529437987301839931281) * 10 ^ 70 + 5975817605372878980103282239300615220689637713884975588790383008747033) * 10 ^ 70 + 7675457301750829477585878936194446180647489166400184025753944911797375
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_322 :
Polynomial.coeff recurrence4Scalar1Second 322 = -((((870358974638998068 * 10 ^ 70 + 2418193211716434892953742458412383860043352843891017500237224069873725) * 10 ^ 70 + 7205236846638786245841997043923928883322940117427339703087814876371703) * 10 ^ 70 + 5611668791507559542490608772500606504170613058436999751478565549419685) * 10 ^ 70 + 8550958379540096172648481901764460461324420410870840969321331853006435)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_323 :
Polynomial.coeff recurrence4Scalar1Second 323 = (((414549861077786904 * 10 ^ 70 + 8641168617075850781825592610653892701901775867636470834105501221261479) * 10 ^ 70 + 6024344650680363773848254935944954495650032413685621770671168935655329) * 10 ^ 70 + 4022982486020332131962967992702737796837122725647251617266373458808433) * 10 ^ 70 + 2288738617778695784172315861580015047561259230723277017290351658790811
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_324 :
Polynomial.coeff recurrence4Scalar1Second 324 = -((((191189816485422398 * 10 ^ 70 + 1718008314104956123800538493917005908315445898436579393078092621711306) * 10 ^ 70 + 8661581490658727035305937668066461303152516235548217991143816346608818) * 10 ^ 70 + 2710323830127546345006481894745943247236582314941999332664780725790600) * 10 ^ 70 + 7248223366954840034984260391074760151029492190965790022081904361612726)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_325 :
Polynomial.coeff recurrence4Scalar1Second 325 = (((84888451501799104 * 10 ^ 70 + 8648780486574059518950333945104627994653861344452870649803491677189118) * 10 ^ 70 + 8116070860625897994313424368558881529819564910641045896107428038920532) * 10 ^ 70 + 9527981551933038572152482409760597296902970635296358700743323778420912) * 10 ^ 70 + 113985777275805680013226534269762744405601818128314087596195152341643
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_326 :
Polynomial.coeff recurrence4Scalar1Second 326 = -((((35950791369016447 * 10 ^ 70 + 8137101259747827141404626161308693796257586757813562846088423910961929) * 10 ^ 70 + 184858063974856454239447110869672910122384235580429388962174374410040) * 10 ^ 70 + 1757384057710486250917968792311747364258474360913016355394991637997501) * 10 ^ 70 + 8421779152247678238487600066686512496048930073339321511081524586276800)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_327 :
Polynomial.coeff recurrence4Scalar1Second 327 = (((14290256198521147 * 10 ^ 70 + 9735963265294864743356669767542109464399749252096320219444862871266091) * 10 ^ 70 + 7262437246790801115271620723871142454468780816286098022253098124966807) * 10 ^ 70 + 7958802379419712649026980594432277236846859916618025836623370759698548) * 10 ^ 70 + 4986496774077347887508229821439400736794996046429148839942023383714335
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar1Second_coeff_328 :
Polynomial.coeff recurrence4Scalar1Second 328 = -((((5163088577551240 * 10 ^ 70 + 5681162853197878874627298211083938557784325440639363761768444112352193) * 10 ^ 70 + 2937832282357803756160003213587559726764644465443761033983735841979958) * 10 ^ 70 + 246765845110892441765199617480305701041746362367688539546103354881945) * 10 ^ 70 + 1520748463010102283822773962628792410785618646236194356789461412145214)