Recurrence 2 lookup certificate: Scalar3Left coefficient convolution #
This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_187 :
Polynomial.coeff recurrence2Scalar3Left 187 = -((44203709569798262383441489807379029446576246737197765105368 * 10 ^ 70 + 1335350874107270307791090438106763383881427557235837363919121233748963) * 10 ^ 70 + 359679474781776427392238117580726650242169290976983966500224551372167)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_188 :
Polynomial.coeff recurrence2Scalar3Left 188 = (84079351629718217126975018744516601785703335270221673301674 * 10 ^ 70 + 9935402896435265844158454142519502519220334531942940127702129105868753) * 10 ^ 70 + 2392920549350469922349903852905647678446208216021525042128813558431162
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_189 :
Polynomial.coeff recurrence2Scalar3Left 189 = -((18422394908845200963377118181905805727922185926556892683408 * 10 ^ 70 + 7522437427181574870557715917764738076260993920575685583455677278489794) * 10 ^ 70 + 2868635382354483591265665201179338963289064150189173693062768969840313)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_190 :
Polynomial.coeff recurrence2Scalar3Left 190 = -((503204825765916880358215966482166088987782443236866932776551 * 10 ^ 70 + 8721380988346082010338583630902046659424941301618598397089346060317563) * 10 ^ 70 + 6367356094044166635204483885695787237220994202565272334784127698903872)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_191 :
Polynomial.coeff recurrence2Scalar3Left 191 = (2076127411424407519283045498940114093362019472703458026155428 * 10 ^ 70 + 8054602248649652508782279122509308854638333409770987611111307055211819) * 10 ^ 70 + 4939204890100799802437775670066847298214195167836787515896534830134486
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_192 :
Polynomial.coeff recurrence2Scalar3Left 192 = -((4740016516465735681954618106342473905087002749144995210065335 * 10 ^ 70 + 982321432439283246572464528953929416785675621044381496457525127574969) * 10 ^ 70 + 2017234988136429787894077194511148912110628223197577919059691749186038)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_193 :
Polynomial.coeff recurrence2Scalar3Left 193 = (4958971102841599687613218093887891380138079757847063336135740 * 10 ^ 70 + 5547452252647748648807866375690118997639620222384744368861461778738710) * 10 ^ 70 + 7701775251741079592290671675241550985781378646077437856106974279151491
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_194 :
Polynomial.coeff recurrence2Scalar3Left 194 = (10877699015226361862598848364604978194873224522562005911897301 * 10 ^ 70 + 6507864315812575916348267045635602851495316040995978953123012771659000) * 10 ^ 70 + 5359611110294182954017648193934559252671180423195167772003875864990825
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_195 :
Polynomial.coeff recurrence2Scalar3Left 195 = -((73178856958939072512004366711072029849449244136783677878588087 * 10 ^ 70 + 3845788913081636183003985875879772914075678161602716214692563554644540) * 10 ^ 70 + 242353085162505972172329540356668425157576871760093298002634607028781)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_196 :
Polynomial.coeff recurrence2Scalar3Left 196 = (217495924206605931383876827477931466858787418521136662638393406 * 10 ^ 70 + 1187854562204051856085894418305070101933612507591136719777654027268277) * 10 ^ 70 + 366494554893519992189399340172740337659763733636906749572992883903626
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_197 :
Polynomial.coeff recurrence2Scalar3Left 197 = -((404515122042726264628653339687635884073322735909466334255176907 * 10 ^ 70 + 581539185544549738347145717635414941126779653311441919863421528568671) * 10 ^ 70 + 5297193937403711287649880093759446226895441769439616039009508359705369)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_198 :
Polynomial.coeff recurrence2Scalar3Left 198 = (287573163175405497175451200946458242278623768494599176960041295 * 10 ^ 70 + 4066946357562701033336824853697411160605004868540665607197365843889350) * 10 ^ 70 + 6177742800713570319212138691918788940427343009793909123533304029592929
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_199 :
Polynomial.coeff recurrence2Scalar3Left 199 = (1223516505155803165352763085635717041601932313999418022973504981 * 10 ^ 70 + 936693909527475369410646803520732352654290687782475342381149932233958) * 10 ^ 70 + 7713743853742844405729548100900935651947572014241456213209535883329382
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_200 :
Polynomial.coeff recurrence2Scalar3Left 200 = -((6374597035731691707618123826051929272771278442928298672437063671 * 10 ^ 70 + 5419800202215632999432377044448580302683383569609196512892383792022570) * 10 ^ 70 + 9048261135319056243599992011151193562749290452966899623411794556899532)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_201 :
Polynomial.coeff recurrence2Scalar3Left 201 = (17900453232542661986566390065072740470921990593266759186781358059 * 10 ^ 70 + 1359148255798751165898854425394861153483190601488168723733593239224846) * 10 ^ 70 + 813612898264725809286546422455634134948941559288058221317639632850070
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_202 :
Polynomial.coeff recurrence2Scalar3Left 202 = -((34587644042605756211331762217047792246891572873164131075910305064 * 10 ^ 70 + 5613174072927244344171934215722864917264290817023508763179675045566167) * 10 ^ 70 + 733458245679079377017623732775261798345955109194362954211741882964967)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_203 :
Polynomial.coeff recurrence2Scalar3Left 203 = (38285560964705961454276945023849618320740098644954688355280772317 * 10 ^ 70 + 2210338214938906870090006870737754876773988965032724403813789653568892) * 10 ^ 70 + 2661450295949604948410789031229344419327276317300163578668894675536678
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_204 :
Polynomial.coeff recurrence2Scalar3Left 204 = (32753808373605642654587346042600764170577016191003378467539657733 * 10 ^ 70 + 5871074377316116394477460924962448638928745229287267026655089519024658) * 10 ^ 70 + 1779894635206517565475971237568013989669539522428662614462883244865150
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_205 :
Polynomial.coeff recurrence2Scalar3Left 205 = -((322044599572493349459435680853838758496858912034918178063122393876 * 10 ^ 70 + 9400395158698691155835258515895330186093138731439429100587165607438091) * 10 ^ 70 + 4636156281017427634279793293658854916850580985406220375047927828058541)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_206 :
Polynomial.coeff recurrence2Scalar3Left 206 = (1076439547243174890860341562056211700601002235803193758826668744497 * 10 ^ 70 + 4702009542861772444559421850471201318663397444945091577100057274730933) * 10 ^ 70 + 3449091755628830082772776518405574208031969272660414662121646868264574
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_207 :
Polynomial.coeff recurrence2Scalar3Left 207 = -((2563303769105782231382905275598812040894774052615008978697658689298 * 10 ^ 70 + 9440886372261578851496816238135359293057114055532425238178733694677104) * 10 ^ 70 + 6483215861251367353159910727273265677546744463872352368489636372986101)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_208 :
Polynomial.coeff recurrence2Scalar3Left 208 = (4690372890582882837759177581863947981005515651751342467295617289531 * 10 ^ 70 + 6412723421877717027393764700605561442515961636074227175294816987562400) * 10 ^ 70 + 8583659114129006453231583919553483309329206426562141491668109795049042
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_209 :
Polynomial.coeff recurrence2Scalar3Left 209 = -((5994342997198344220908444026473957533790438167126104131679037889917 * 10 ^ 70 + 9002081599635377340588764564791727453569089162774387515328324738994382) * 10 ^ 70 + 1569483024294032133142320876291421296533266430847189989736960120726241)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_210 :
Polynomial.coeff recurrence2Scalar3Left 210 = (1546295036431269765094075984610327764636747082621176918581257503543 * 10 ^ 70 + 4951094271836104648746735858520541174976044607557609509601118168898388) * 10 ^ 70 + 2320538173438008679088253682712822767475586121695943489745165270161838
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_211 :
Polynomial.coeff recurrence2Scalar3Left 211 = (20633660267231202777650295921258405189275827601006514212046929926142 * 10 ^ 70 + 182654878245852373941269530372140805108549471362095952344843175178053) * 10 ^ 70 + 4975180626580528504739879171255130442254586818332632164331477001951516
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_212 :
Polynomial.coeff recurrence2Scalar3Left 212 = -((84623331349272367417659741974117242775037047386293894171454816185053 * 10 ^ 70 + 7118140242693606726865873754099190543597761275450603836502718793050201) * 10 ^ 70 + 9459527109329180734481121083289920620180162093055309209381361632900388)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_213 :
Polynomial.coeff recurrence2Scalar3Left 213 = (231969826721574570985042686702972940431362720014801854622807289603741 * 10 ^ 70 + 2776197875263420550094452912784307585790966009625363266238969604859266) * 10 ^ 70 + 3709179884544168677022332526022281565684216292309814883032638831902552
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_214 :
Polynomial.coeff recurrence2Scalar3Left 214 = -((524272565936183315139545469564864207238570473652674861969632763073206 * 10 ^ 70 + 708183798095507406540938324288577884217142795004825284210591171812740) * 10 ^ 70 + 5084236065115033855562520452308269644059337522379319867753387488813721)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_215 :
Polynomial.coeff recurrence2Scalar3Left 215 = (1037133011169919019916550123488444517588263744240001948518561186130993 * 10 ^ 70 + 8195695251906723961543511481868519338054731747016066682213578674917408) * 10 ^ 70 + 9652233178598456753528787438965969828060357144616244365760726976672300
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_216 :
Polynomial.coeff recurrence2Scalar3Left 216 = -((1836823839393470265927672978162225732528426146028722502483827656009715 * 10 ^ 70 + 8930760163575529126224573302756249201605554862787082936529487119958567) * 10 ^ 70 + 6943287727462092294443703786143495790493961315630393435398396170387178)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_217 :
Polynomial.coeff recurrence2Scalar3Left 217 = (2929593186358274839608540574857125548500100888502489841024429802890803 * 10 ^ 70 + 6680084797745707869987643886514920155125228297342651069417559430617499) * 10 ^ 70 + 5855773655774657603507082917719621011475298828342703011587749312492459
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_218 :
Polynomial.coeff recurrence2Scalar3Left 218 = -((4175516073099543405988764636651511178188096870989736646180577059507268 * 10 ^ 70 + 2842360040068889832517942008849125653619346108363634272277408015350686) * 10 ^ 70 + 1958881596240635090147682158402111625325292520013637402578146274544583)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_219 :
Polynomial.coeff recurrence2Scalar3Left 219 = (5166347002885056999871461016635850076502373679296507502962913185601729 * 10 ^ 70 + 7542646227295638626888521096472398281926500476497252398230932545603599) * 10 ^ 70 + 9495762640470964743939673460938211987595695326417358497438761735534436
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_220 :
Polynomial.coeff recurrence2Scalar3Left 220 = -((5080976225576140416604125185948372489646449771376614589703027871296282 * 10 ^ 70 + 8985149156468680185554127391796835721928575735325397065702151438031091) * 10 ^ 70 + 8873394715164793157326756429013784062781754126856591907802883699108805)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_221 :
Polynomial.coeff recurrence2Scalar3Left 221 = (2551510481048550534606189079548737317640637770207274197361238765632801 * 10 ^ 70 + 3798076909110150809326400941594181018187600960972410897272305010092173) * 10 ^ 70 + 93143482948105416286532016689755861648530929257367541867263431945150
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_222 :
Polynomial.coeff recurrence2Scalar3Left 222 = (4407067737681488604547761961191611789270612456961679326049785845644542 * 10 ^ 70 + 7020119356399664001158744997433504056686345050208676728318022415993311) * 10 ^ 70 + 3888612892147513058792421771006938876909717036772377736143217149357556
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_223 :
Polynomial.coeff recurrence2Scalar3Left 223 = -(((1 * 10 ^ 70 + 8338350572577790127136387774287903991314461788202072726916185977677852) * 10 ^ 70 + 5426853360412256961961687912300642158205832194339516314411314445976827) * 10 ^ 70 + 8335579350417423921454839148616585882661773860549370259606801352575314)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_225 :
Polynomial.coeff recurrence2Scalar3Left 225 = -(((7 * 10 ^ 70 + 8378449922655530716721485057121098384452960145759616407426825405412980) * 10 ^ 70 + 5077748133669114631439900744331773728053792293595906751102923170874982) * 10 ^ 70 + 7775349863561930849123967734999730856423013238354151131493490436780769)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_226 :
Polynomial.coeff recurrence2Scalar3Left 226 = ((12 * 10 ^ 70 + 9059036281384068438293571149933138857365766049526651627072739146838999) * 10 ^ 70 + 4496537123728190837750029109027422953011336989037460580050437253276202) * 10 ^ 70 + 8476062279957931146293180190432012130684462704437544931120517743661290
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_227 :
Polynomial.coeff recurrence2Scalar3Left 227 = -(((19 * 10 ^ 70 + 4428562507529442144852294126991473117667961233412694329746079809753237) * 10 ^ 70 + 5542338295034303220325017788438997479162150204877583209539623298954940) * 10 ^ 70 + 3518210876526246878708196404333968568439457977474545924787971373854672)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_228 :
Polynomial.coeff recurrence2Scalar3Left 228 = ((27 * 10 ^ 70 + 2496113842970695387308025306533868962834229517293822797119116712492894) * 10 ^ 70 + 3200403598442786745149312001326869242271529682515406911385417932770762) * 10 ^ 70 + 940458606822632212422215426617001416293374031805870697389440513476515
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_229 :
Polynomial.coeff recurrence2Scalar3Left 229 = -(((35 * 10 ^ 70 + 8567583539444707991236080546864842879813083882898707362072063534466279) * 10 ^ 70 + 9152598683735344172911490959446873117728372980392826881394275017471586) * 10 ^ 70 + 7077645428309867303961647823488322177790485492208204716279168393937880)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_230 :
Polynomial.coeff recurrence2Scalar3Left 230 = ((44 * 10 ^ 70 + 5293600164337820276125087012375970645096872185225016298836517611404647) * 10 ^ 70 + 3889807609615151814506193179366646599939473237723816007547002245342573) * 10 ^ 70 + 3294572321614508903010427608719150582222144620835192582054519619143012