Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1MainPart1.Coefficients268To302

Recurrence 2 lookup certificate: Scalar1Main 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.recurrence2Scalar1Main_coeff_268 :

Polynomial.coeff recurrence2Scalar1Main 268 = (2850855412284261112541127796750837362668930933195934142022676354875990 * 10 ^ 70 + 3425839561222934431838164546486101504119379815113029228797349175511642) * 10 ^ 70 + 7653107663967007062963510273656280515276323406666963645932126441685165

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

Polynomial.coeff recurrence2Scalar1Main 269 = -((1501161363940334117452534989571242968269853496037744340902356991079586 * 10 ^ 70 + 8691691443830486675456250003178723464911720173952827431116047477219704) * 10 ^ 70 + 5348690114383445096688067987404954177476450308739507934752195729185742)

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

Polynomial.coeff recurrence2Scalar1Main 270 = (736810254474570667981011950294452029644752799417782076711519209010071 * 10 ^ 70 + 9176892113056028566639503606715818576382553225102593926723280572194900) * 10 ^ 70 + 3484117249824340315118018814111467309080389090031167732522094197970889

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

Polynomial.coeff recurrence2Scalar1Main 271 = -((336716860643311187904119261871227913154184945640115411215739449661088 * 10 ^ 70 + 6872769355599619376477147278707128527214439911210517682790004249737417) * 10 ^ 70 + 5747027244825687469805921997898945790529674724296189506553013421616100)

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

Polynomial.coeff recurrence2Scalar1Main 272 = (142425464824336095768517446374309681850778085398291952797737398609307 * 10 ^ 70 + 4203521497943829872738915668614285644818289977021602707268561451941036) * 10 ^ 70 + 7619754238050749215642628284031636460238025894357613861746827143883823

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

Polynomial.coeff recurrence2Scalar1Main 273 = -((55035562196597543987176233992871898155518834056950048330268172739130 * 10 ^ 70 + 8309645890636753036309199082355155025487301684146921508144084483755196) * 10 ^ 70 + 8780424458027741138818739754389121252151698120013271578952434090650340)

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

Polynomial.coeff recurrence2Scalar1Main 274 = (18899398206752627882080416614269318177238133125273261790768326019463 * 10 ^ 70 + 9056353486406769863897890214924673001918503124177628118508274504188857) * 10 ^ 70 + 6705650625443914580624960610128887531008541185423445177287423282164646

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

Polynomial.coeff recurrence2Scalar1Main 275 = -((5391317214225823837712024842176323684981513970269230532922731525387 * 10 ^ 70 + 5750542189348598296801761828644902917544550777644478482945476829492550) * 10 ^ 70 + 7251900790177192303783554514430256712793505258511802601521948369763957)

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

Polynomial.coeff recurrence2Scalar1Main 276 = (994545162421502892142741666234195017520543141908839298644190041251 * 10 ^ 70 + 4867089259571189692767271082307994090171694925872696924911705416087429) * 10 ^ 70 + 5372732106704294126491518265040603784183273102895354493358558394680645

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

Polynomial.coeff recurrence2Scalar1Main 277 = (129424278660425829708129643005450311972547842629810643340904506848 * 10 ^ 70 + 9949759061269019244263615006651924644078099500998921026408276805715152) * 10 ^ 70 + 1927968180984249526480971452290423382246311867218056388394154519216580

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

Polynomial.coeff recurrence2Scalar1Main 278 = -((258712465291153515655283933284322179217634898045186084747496766206 * 10 ^ 70 + 3112919456766007728572394230379271487320314674705959644414771104438547) * 10 ^ 70 + 129928130706592987173516959013564960917315537116922651230415083956886)

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

Polynomial.coeff recurrence2Scalar1Main 279 = (172642493292449970986387477371328561648024592621263102448902485091 * 10 ^ 70 + 2926935663040752963774449302430002432749959179290710400332053985732896) * 10 ^ 70 + 4570868672472161169893319598794700234446125004284339964635473488318388

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

Polynomial.coeff recurrence2Scalar1Main 280 = -((87299628137639065260345897534652138566446612510974685037166693539 * 10 ^ 70 + 9529648097877103800674248683327238394157865737991526726635438434337663) * 10 ^ 70 + 862404392139029840392978927643664412277662781776561832576005814683958)

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

Polynomial.coeff recurrence2Scalar1Main 281 = (37549067975713914515180842524728158646799558771930275490647191561 * 10 ^ 70 + 9616811464184501813098744090221886931583939386113778147716725180770714) * 10 ^ 70 + 9685271300064449520925885125930645637635403954207436666089459969201055

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

Polynomial.coeff recurrence2Scalar1Main 282 = -((14196650164562921051398384718435149006306981391391574664247081805 * 10 ^ 70 + 8299052233263002111256180930594923387147722381467782444520577445298329) * 10 ^ 70 + 3786476595359660735619927987355927363510575964141159806967301108539290)

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

Polynomial.coeff recurrence2Scalar1Main 283 = (4733314286758572344259926499319301374406967109529122992553178964 * 10 ^ 70 + 6852761876512912308990472509717155348995784240935946285267265179505039) * 10 ^ 70 + 190454660663983046783325347351842614642127238192378283775762266279425

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

Polynomial.coeff recurrence2Scalar1Main 284 = -((1361823158738373057708686663086270712877261879484701911602374874 * 10 ^ 70 + 1488905029552826664291322678600437747540416519094741618018539177551379) * 10 ^ 70 + 9973561975105692790267768382567362419379752265750833351807335718101867)

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

Polynomial.coeff recurrence2Scalar1Main 285 = (314340129623809720058986736655714452866323753079787834674995188 * 10 ^ 70 + 6598323860604876882125153085526954544783559618566863955288711564104956) * 10 ^ 70 + 7099674405846087386532501925593378705627782821364922596615590972459474

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

Polynomial.coeff recurrence2Scalar1Main 286 = -((42346798274584055402423971232373785910480013102976623821296903 * 10 ^ 70 + 1868123046476783425965076726252031808627321099047096841718125295620640) * 10 ^ 70 + 7437151513716105581972655984070136158287050707706778023195743993070061)

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

Polynomial.coeff recurrence2Scalar1Main 287 = -((8448459515209850240129975589634922907937431342116310541321334 * 10 ^ 70 + 4616302399068533884322549132709971184834852994313684322090691776684422) * 10 ^ 70 + 1048776765334511323080611620440892931898966961493256964780490374075075)

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

Polynomial.coeff recurrence2Scalar1Main 288 = (9564418461556564080338469216715565941078028633476547005303998 * 10 ^ 70 + 6189742597067852944910032923681508580120971480480632513131727164750925) * 10 ^ 70 + 7725397771341033840422909374821033181879899553543224101315135842240185

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

Polynomial.coeff recurrence2Scalar1Main 289 = -((4781853560933460282268599980131162425305716234506896620412398 * 10 ^ 70 + 7102497933713025858666944393871527126399047723022285332662148039210753) * 10 ^ 70 + 6852497566860927016354049742909579019743821162107354844678875855434367)

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

Polynomial.coeff recurrence2Scalar1Main 290 = (1825772567181622408888828879686061854282945475774746289576205 * 10 ^ 70 + 3682580412821317511413829153010247534692684513288486476579504683699480) * 10 ^ 70 + 1690085572929324121140738806477030228143666365616556479814870002009118

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

Polynomial.coeff recurrence2Scalar1Main 291 = -((582661673821073134056758650099139936192452506588190347559494 * 10 ^ 70 + 5998129070559970845144183122445241159944681320871223518509755022471352) * 10 ^ 70 + 4621057965285059614333568546218909114593035555062519083998071009519774)

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

Polynomial.coeff recurrence2Scalar1Main 292 = (157675796589385745818184953580923832647125089792298930658333 * 10 ^ 70 + 7156333218209992460231824402891023846268772549451857892468474850661424) * 10 ^ 70 + 640683549290821858990622903621635899617977456820152717152926708594483

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

Polynomial.coeff recurrence2Scalar1Main 293 = -((34993392372852520361014026364165879436995100084400884209989 * 10 ^ 70 + 7755831963600423491141361136893308065713400593023776727049042299990272) * 10 ^ 70 + 1460624175721310304666050927187326935576906606052883763918980266727095)

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

Polynomial.coeff recurrence2Scalar1Main 294 = (5499014363414545100441070587327933787305697885375114671571 * 10 ^ 70 + 9994066017023365405596683854151660665202394372144718378020737178381643) * 10 ^ 70 + 7834941516589754526291414345450963956380281359587118872503974906977982

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

Polynomial.coeff recurrence2Scalar1Main 295 = -((93947995978641353513209067174306169658959799266052874766 * 10 ^ 70 + 8447958272236654213403638903795862087720701008584953008265366790813269) * 10 ^ 70 + 4192554670070086102007306528389879097541986236849570014592536459036508)

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

Polynomial.coeff recurrence2Scalar1Main 296 = -((358863361577996794926444504259845714435000061754526269254 * 10 ^ 70 + 850490098458858531954405263228718580970866117137036837155647952310528) * 10 ^ 70 + 5834361872332106116309519424646991504431420470280021723196566742122960)

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

Polynomial.coeff recurrence2Scalar1Main 297 = (180042488166679987250153330383658020713657175468240789855 * 10 ^ 70 + 5093032605031175649230549006159150889583303761796576172657901204625317) * 10 ^ 70 + 7853702661029962709388074424097116588577077219458144917352200568473914

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

Polynomial.coeff recurrence2Scalar1Main 298 = -((60712431889175839708879414032641464286958290376615203510 * 10 ^ 70 + 2816274825456896741546177360781082588843546272118316511700783425047411) * 10 ^ 70 + 3596036183958334340614167020804651589298161792625606000145906766046220)

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

Polynomial.coeff recurrence2Scalar1Main 299 = (16340618812940849143858239144736832302836816820641179661 * 10 ^ 70 + 4353835512762809099832672326018258379586643334935604748080051038702810) * 10 ^ 70 + 5671904492047372688297712554835143535159257781801209019870405387763205

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

Polynomial.coeff recurrence2Scalar1Main 300 = -((3602770613208671621692352835907724218225422065627290467 * 10 ^ 70 + 7132773395513625788660664426004446796496670035357336315897142012602347) * 10 ^ 70 + 3044504774543915705804626541632323835054093986095420327577464522689653)

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

Polynomial.coeff recurrence2Scalar1Main 301 = (619510495808592158973438994538738099139336561947379121 * 10 ^ 70 + 386421820138117367859835779159498337197395975874476325468038028029309) * 10 ^ 70 + 731861716817861823699863229574370751642009514481428365142096585581417

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

Polynomial.coeff recurrence2Scalar1Main 302 = -((63404785606077160970656125540592821508516343799233090 * 10 ^ 70 + 202365278386016719938943976326256424682087597885487968168204471203929) * 10 ^ 70 + 1448283297410615870160855140580400055183655945772657938264091795133116)