Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar0MainPart1.Coefficients340To380

Recurrence 2 lookup certificate: Scalar0Main coefficient convolution #

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_340 :
Polynomial.coeff recurrence2Scalar0Main 340 = -((494219462828144338103 * 10 ^ 70 + 4102098471322411246225289896608929383758375272298614605715274621689162) * 10 ^ 70 + 3948921852712205251927880487877725745014830655814561508752840419852559)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_341 :
Polynomial.coeff recurrence2Scalar0Main 341 = (23516903396949653512 * 10 ^ 70 + 1742546516110390304967136170903102881007927892819012076363455812798776) * 10 ^ 70 + 45939865423566752530861195873941025203901601514661021668872626678100
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_342 :
Polynomial.coeff recurrence2Scalar0Main 342 = -((550568247048044873 * 10 ^ 70 + 6847831493317172176691086891946239376220396186364542335716319427349995) * 10 ^ 70 + 1259187597441738280200218855424437431492712542643437085072587831850770)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_343 :
Polynomial.coeff recurrence2Scalar0Main 343 = -((5732490478207690 * 10 ^ 70 + 4424962135252817182430850885258721552920905260993744223586791221294751) * 10 ^ 70 + 9668309568939981708776587269570762599523814249298264806049477299163205)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_344 :
Polynomial.coeff recurrence2Scalar0Main 344 = (991165877963773 * 10 ^ 70 + 6598612511077916435498639046259759232768136323525125796797009104287400) * 10 ^ 70 + 1991209950413194182852426168779892222101081919125274976411461656430983
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_345 :
Polynomial.coeff recurrence2Scalar0Main 345 = -((37460510217084 * 10 ^ 70 + 8740269032486953419779362618789573898903999445601257382693315776050296) * 10 ^ 70 + 6016762727697697325696880050227519136777357259370492244248017474842334)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_346 :
Polynomial.coeff recurrence2Scalar0Main 346 = (602726363600 * 10 ^ 70 + 8610958578091907038451716372668129121573817631895324330419097426630128) * 10 ^ 70 + 5343559545379647073732719043526857390167110367578630058239646355753583
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_347 :
Polynomial.coeff recurrence2Scalar0Main 347 = (4818180109 * 10 ^ 70 + 282399638340542799617167720883402601546843559163293573660239296212413) * 10 ^ 70 + 9825950639676733065781613111687127827450043318921975478457673734063049
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_348 :
Polynomial.coeff recurrence2Scalar0Main 348 = -((438609170 * 10 ^ 70 + 9325128333910737824508385194280342896057428451800293918722851114803561) * 10 ^ 70 + 4576335687533747032355555016690232337089829500572258651247790251710717)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_349 :
Polynomial.coeff recurrence2Scalar0Main 349 = (8172799 * 10 ^ 70 + 6123950012413100727412265048509019479547538554460281691031128174272450) * 10 ^ 70 + 5964258203809941920987455157749944980070927143120632540925494289240835
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_350 :
Polynomial.coeff recurrence2Scalar0Main 350 = -((23267 * 10 ^ 70 + 4628521806977063470876036524762528813453373893789800010473281556938989) * 10 ^ 70 + 6399679120100715463612576112817873889487590909168692698676188524365489)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_351 :
Polynomial.coeff recurrence2Scalar0Main 351 = -((1474 * 10 ^ 70 + 3440780243574919296972273007760464438752055502123773498790673852833363) * 10 ^ 70 + 6193102591921077265811337102588110885102768725480386202841717884163513)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_352 :
Polynomial.coeff recurrence2Scalar0Main 352 = (21 * 10 ^ 70 + 2319869042841115332880682790464275624649178337450999649048442870876137) * 10 ^ 70 + 3152565117386951211005041426006863859820283065959362586624600428693468
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_353 :
Polynomial.coeff recurrence2Scalar0Main 353 = -(31293305372524676557024745891150639522031810876573554137338255900419 * 10 ^ 70 + 1400049358796524351528577414152284130709117878747270515747359021638320)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_354 :
Polynomial.coeff recurrence2Scalar0Main 354 = -(20713181893015623223490139033488029385354044770738416312170604417924 * 10 ^ 70 + 8416239031422164179697056284921953884231071073598762761133828932634812)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_355 :
Polynomial.coeff recurrence2Scalar0Main 355 = 110115340402840154865553103125902939853749353528398827795724402750 * 10 ^ 70 + 2694590752648494252248475709608239288617568652128895827701050713255965
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_356 :
Polynomial.coeff recurrence2Scalar0Main 356 = 807802576320769060018416726648574115874535301145506652419373637 * 10 ^ 70 + 5383987404582063476412937776634467207436125219317876193557798969276968
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_357 :
Polynomial.coeff recurrence2Scalar0Main 357 = -(7642155161662610694273497010626492611461786383449668185377454 * 10 ^ 70 + 459380178364082726202922136228816741973317109549459694194382475701292)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_358 :
Polynomial.coeff recurrence2Scalar0Main 358 = -(11484927350220148619996609389725716204560373384835391534109 * 10 ^ 70 + 949066629279796549881581339673975092793038564521011137744842973036073)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_359 :
Polynomial.coeff recurrence2Scalar0Main 359 = 243081737553621215362462167095323802522190806198602791555 * 10 ^ 70 + 4592742559305681876444609197349537756287242024594767639452676402270919
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_360 :
Polynomial.coeff recurrence2Scalar0Main 360 = -(138804389074159281090912221504217485860870246230685047 * 10 ^ 70 + 3056675631947611399146000121378956202356110471986372371167678793756460)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_361 :
Polynomial.coeff recurrence2Scalar0Main 361 = -(4127928039976001239078008300550326244775302801577056 * 10 ^ 70 + 2021130671270522795008822251389023581832700917948751789543805727180700)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_362 :
Polynomial.coeff recurrence2Scalar0Main 362 = 7516384151683937787778104407643644383674606114027 * 10 ^ 70 + 8368942816472671629091426918855910895054272354278348836171572170272503
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_363 :
Polynomial.coeff recurrence2Scalar0Main 363 = 35693243381444906732477312621541486900736908338 * 10 ^ 70 + 6585715767980465951793869718895550325069398657943638388981673336294067
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_364 :
Polynomial.coeff recurrence2Scalar0Main 364 = -(110661762651615480700279477369175679514127153 * 10 ^ 70 + 7073112234869762446999581661179269438344621139641457042003231155013853)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_365 :
Polynomial.coeff recurrence2Scalar0Main 365 = -(99441347900275471119781165560335029671744 * 10 ^ 70 + 1691886432001220531170639503400153333343963922416283361033135653615874)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_366 :
Polynomial.coeff recurrence2Scalar0Main 366 = 707009597677409764962189289177047336962 * 10 ^ 70 + 9905707547758718351563195201808774554379607875789696488813424252794879
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_367 :
Polynomial.coeff recurrence2Scalar0Main 367 = -(520221376803460516007277918430586827 * 10 ^ 70 + 9236935853536561204593857298200256064643407371277652599371886250461208)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_368 :
Polynomial.coeff recurrence2Scalar0Main 368 = -(1425192709617654737711715490143204 * 10 ^ 70 + 2289481218137458000486012190902134419248824451550166496752033455185120)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_369 :
Polynomial.coeff recurrence2Scalar0Main 369 = 2939061307591349242762614257357 * 10 ^ 70 + 6448155083997660530491465790219818833598914937035043631559617669036109
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_370 :
Polynomial.coeff recurrence2Scalar0Main 370 = -(1613538330456372640861305011 * 10 ^ 70 + 153597802944230981951526150879124723292395520760967858238668700815727)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_371 :
Polynomial.coeff recurrence2Scalar0Main 371 = -(630556026267691223268693 * 10 ^ 70 + 8871626874478879965560044674492424811090626234317765278418040840715208)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_372 :
Polynomial.coeff recurrence2Scalar0Main 372 = 1118850555038714489169 * 10 ^ 70 + 9441604927502213587793681438815520655932030274406819513044145495576504
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_373 :
Polynomial.coeff recurrence2Scalar0Main 373 = -(478594372476479166 * 10 ^ 70 + 9657305567123953716575749643148400785041372009007239436980388473511261)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_374 :
Polynomial.coeff recurrence2Scalar0Main 374 = 74331233785978 * 10 ^ 70 + 4872815122769136173505292187011550314785444772333065661889836521392286
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_375 :
Polynomial.coeff recurrence2Scalar0Main 375 = 1044075029 * 10 ^ 70 + 3625593090230223430597511639000228772207868299825451134632266351740406
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_376 :
Polynomial.coeff recurrence2Scalar0Main 376 = -(1302666 * 10 ^ 70 + 6570268961323618135494588441964506434113742164909965754677932648886437)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_377 :
Polynomial.coeff recurrence2Scalar0Main 377 = 110 * 10 ^ 70 + 6602885024047042195664750379155276891893810016577114454916401614756262
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_378 :
Polynomial.coeff recurrence2Scalar0Main 378 = -30097960837772564439873640634145529634968659772731937865085136387159
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_379 :
Polynomial.coeff recurrence2Scalar0Main 379 = 210103072733663624353547674933011945455543547343113810137195418
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar0Main_coeff_380 :
Polynomial.coeff recurrence2Scalar0Main 380 = 1529622938896234486906546024896229387378572985954582070010