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_303 :
Polynomial.coeff recurrence2Scalar3Left 303 = (761253957327360251865539841489674295705706619816 * 10 ^ 70 + 9613348330076283406904244364788901772595126976345778917979056683235529) * 10 ^ 70 + 2404495082299311192685774607361545260142145716247969848069332678208923
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_304 :
Polynomial.coeff recurrence2Scalar3Left 304 = -((41062380566367415104769031419134473970385827574 * 10 ^ 70 + 490845816884440294228333434364037757931356014503642853947324129801561) * 10 ^ 70 + 4346541983533101763571687700186471562553386341654861761968359188712614)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_305 :
Polynomial.coeff recurrence2Scalar3Left 305 = -((10439252697784147358848459005609443627366025402 * 10 ^ 70 + 6172251118619130994264805022850724177838677522208140447337246277188438) * 10 ^ 70 + 8458530680099367728565704436838966526680655151326649112283059215740858)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_306 :
Polynomial.coeff recurrence2Scalar3Left 306 = (4403284776164745346343472048074727662720991295 * 10 ^ 70 + 3977183550604806584212922795176202976887237984590506426145533155838339) * 10 ^ 70 + 6021309710090222495921063255601076468348102285635002974890351428145105
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_307 :
Polynomial.coeff recurrence2Scalar3Left 307 = -((1027032763920642365499380203607936393875457072 * 10 ^ 70 + 769577200943508667092476728278951121352736643575779126865675551951837) * 10 ^ 70 + 1185161299545312966398108562452970185243622603009130273247476369068301)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_308 :
Polynomial.coeff recurrence2Scalar3Left 308 = (183644779003979565813202030697677723099243981 * 10 ^ 70 + 5528725967684921236486111554993299897515023128667603837383721040139873) * 10 ^ 70 + 5216508132380290999004845726685770565356333960512662488707167958055221
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_309 :
Polynomial.coeff recurrence2Scalar3Left 309 = -((26725701864717119057766413647664650127020384 * 10 ^ 70 + 6150283837648040594996849888868813721248400565529105879870118257009122) * 10 ^ 70 + 2353293719002216682618319380460240932904384638247493104302526884330333)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_310 :
Polynomial.coeff recurrence2Scalar3Left 310 = (3134460587360472089986630987896674327194796 * 10 ^ 70 + 2779059369323956578986702649454216519726467523130420901427482498290993) * 10 ^ 70 + 8133503995774707891606766719165787430946246972917017322747343851220656
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_311 :
Polynomial.coeff recurrence2Scalar3Left 311 = -((269269524859673164731720647590863699125813 * 10 ^ 70 + 5785755473501845417425362808767632787953309942905628220462295914567942) * 10 ^ 70 + 3730802449513674372138661436741204446026036068452180355354538335923501)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_312 :
Polynomial.coeff recurrence2Scalar3Left 312 = (9172472325275084848152228239317227073725 * 10 ^ 70 + 6673207490125331151026586735951630509999931764260242682521178155565983) * 10 ^ 70 + 5141445761550192739297001252525857000754116936714444635740135341957880
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_313 :
Polynomial.coeff recurrence2Scalar3Left 313 = (2201818704035461563360984788751648823520 * 10 ^ 70 + 5350564976012306966617595229723056082168571882103531839128615799145377) * 10 ^ 70 + 9393982545472379639087055841938581035217233170449634693595475920732268
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_314 :
Polynomial.coeff recurrence2Scalar3Left 314 = -((601828460418977312534619493122850825388 * 10 ^ 70 + 9036144926869662474963934892786899010773383840656112478181371949057593) * 10 ^ 70 + 8622420234675904642656844697998725477510070026961296991676304523283167)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_315 :
Polynomial.coeff recurrence2Scalar3Left 315 = (92986694166813120889269668839887835087 * 10 ^ 70 + 5355391372163833875268557329872481111792460871053585552089528752942155) * 10 ^ 70 + 3503242982125951123002661126249098565896950692717008654803590868732497
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_316 :
Polynomial.coeff recurrence2Scalar3Left 316 = -((10692630785927242785415202690266844314 * 10 ^ 70 + 6626273743111233868434757936947445944693270212656968673764442796875303) * 10 ^ 70 + 6428802303508110335848885244415674251930510530173931825776437110405224)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_317 :
Polynomial.coeff recurrence2Scalar3Left 317 = (943149179684673184959324392451358582 * 10 ^ 70 + 6186788389357899657105601519425229041238321192264796497114719089492705) * 10 ^ 70 + 8258300950107758457903661302349115184827841267995116339153301743636562
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_318 :
Polynomial.coeff recurrence2Scalar3Left 318 = -((58424696551278950177579529354558008 * 10 ^ 70 + 1352362021630623565014521241378092437469310453248254077085848506510017) * 10 ^ 70 + 6708093844147214262975683616640585183188636592486226008529833194778182)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_319 :
Polynomial.coeff recurrence2Scalar3Left 319 = (1287342362845006016604961380305224 * 10 ^ 70 + 2778110365415998578669571620927917184020228056850822401727122117672626) * 10 ^ 70 + 775740831948844746706968775114967262332128061208699599894465494279163
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_320 :
Polynomial.coeff recurrence2Scalar3Left 320 = (251805025000276477040963575021860 * 10 ^ 70 + 4328883662681218777223493368043918029406352541896056164417924920086158) * 10 ^ 70 + 8098587714666393053371730340709953609374285352303295955151016584432169
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_321 :
Polynomial.coeff recurrence2Scalar3Left 321 = -((43975537118395584560205317241023 * 10 ^ 70 + 4451179525494425891123724517193963115475100649426576741059446006695375) * 10 ^ 70 + 4294519372988077692874570862489804995697710836047236030132954753369284)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_322 :
Polynomial.coeff recurrence2Scalar3Left 322 = (4237559802710584179119951761504 * 10 ^ 70 + 7283295556598931651901248749232756038964543356740971183478986717106754) * 10 ^ 70 + 3595272182976270470273927926247404989762526755607044945172090097482244
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_323 :
Polynomial.coeff recurrence2Scalar3Left 323 = -((282906060721801625513745995596 * 10 ^ 70 + 1717737970774161167504417174767065664906595187713034176717063923158947) * 10 ^ 70 + 109145840149472569176578273630604264618308307160739070110645805596690)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_324 :
Polynomial.coeff recurrence2Scalar3Left 324 = (12277026976628213436952587580 * 10 ^ 70 + 5960880093975788294671806872078102428072690849041031309584194445707144) * 10 ^ 70 + 9602621275915761384718111828001968068996122077796901314556173373836203
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_325 :
Polynomial.coeff recurrence2Scalar3Left 325 = -((138782822996129101447015301 * 10 ^ 70 + 283894890840495876567625095445908844626762020828908077656196857002196) * 10 ^ 70 + 6489799778631997976429291369112586076951024488205978151304556645954219)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_326 :
Polynomial.coeff recurrence2Scalar3Left 326 = -((29321053008182775096941201 * 10 ^ 70 + 2893873133456601261165219053236879936101086558228780734361814230353960) * 10 ^ 70 + 2018908302590179753664376649918877657556487980975878500496447357810789)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_327 :
Polynomial.coeff recurrence2Scalar3Left 327 = (2961824897591133657308599 * 10 ^ 70 + 142734755194193507192385661266739589045205678135303594314562772558947) * 10 ^ 70 + 8647583886252722631968693854640142997470008019122736518716391946109071
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_328 :
Polynomial.coeff recurrence2Scalar3Left 328 = -((159689049752837257470476 * 10 ^ 70 + 936832677675100004988726964509304448424964992039098735977433351444447) * 10 ^ 70 + 2242870570494862366648697498590712469094321697062788205023383468096610)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_329 :
Polynomial.coeff recurrence2Scalar3Left 329 = (5051010503348827041956 * 10 ^ 70 + 3173637394190690247611404741104040835280232938224296522684448387857908) * 10 ^ 70 + 3047633187111043339292511225181289501663664148327812656683259471261932
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_330 :
Polynomial.coeff recurrence2Scalar3Left 330 = -((36665764322236062650 * 10 ^ 70 + 7260457231112352937449018642022680225857664286929653488691531710017317) * 10 ^ 70 + 3260281583962541575463438310218460882003684650405706319777515459935533)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_331 :
Polynomial.coeff recurrence2Scalar3Left 331 = -((5453410402168939914 * 10 ^ 70 + 1408998785833780046207350370170065570712654850143409219942466469754429) * 10 ^ 70 + 6032256793899071108221684969581293273026754935517008329033177165216348)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_332 :
Polynomial.coeff recurrence2Scalar3Left 332 = (321115726500030422 * 10 ^ 70 + 1680930341133258613839592075702995258316640748556422116337659528119481) * 10 ^ 70 + 2075491849514132342852000629723271133944211025509038868144565938364643
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_333 :
Polynomial.coeff recurrence2Scalar3Left 333 = -((8805971967721504 * 10 ^ 70 + 9725452212470915083927102570010759232889209470394776077583416737757582) * 10 ^ 70 + 2025098484297415608322643459715575631208304354474706667706478029623914)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_334 :
Polynomial.coeff recurrence2Scalar3Left 334 = (81794875615493 * 10 ^ 70 + 4187793055099502159356253086306382105154093390670825099179371355388998) * 10 ^ 70 + 4873702602152140431326879718605050898389127117054231936103686227502607
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_335 :
Polynomial.coeff recurrence2Scalar3Left 335 = (2887634848562 * 10 ^ 70 + 3598338502890369755009191080306269186140230209546798638146484594003156) * 10 ^ 70 + 6511824387225831188803095295976336508083834819848475461241009811262942
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_336 :
Polynomial.coeff recurrence2Scalar3Left 336 = -((121207045541 * 10 ^ 70 + 9291131149536822432029818382807876972674871639841569553653614644254585) * 10 ^ 70 + 9190911733303274606697843215018008761285266624773687946415586256625035)