Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1ShiftPart1.Coefficients339To380

Recurrence 2 lookup certificate: Scalar1Shift 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.recurrence2Scalar1Shift_coeff_339 :
Polynomial.coeff recurrence2Scalar1Shift 339 = -((16866125152116142 * 10 ^ 70 + 9683497052977959773253181942828297137746640013362930304847842381487551) * 10 ^ 70 + 2817086919675934780948365497727074355779421968153995506290383061166637)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_340 :
Polynomial.coeff recurrence2Scalar1Shift 340 = (482156108910704 * 10 ^ 70 + 8165048589111055125124008573380449861774863732362649637735573162746701) * 10 ^ 70 + 1564435793977507975141988700604588667002344221967672918188992424378159
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_341 :
Polynomial.coeff recurrence2Scalar1Shift 341 = -((2251466810938 * 10 ^ 70 + 428611007815924796895273185192742098220971201313452682552509233265018) * 10 ^ 70 + 5673004308403452443682403353408905374035652569542425958837005740755458)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_342 :
Polynomial.coeff recurrence2Scalar1Shift 342 = -((356677035091 * 10 ^ 70 + 3679047804760357409428227392918422767589863854979445929390684262993796) * 10 ^ 70 + 1146466911598224765013827694802754397982859499935346310275623475926109)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_343 :
Polynomial.coeff recurrence2Scalar1Shift 343 = (13547820471 * 10 ^ 70 + 7316693191835205197325473353817279650161139523074865746130564798129336) * 10 ^ 70 + 3513814035338899032077895594999978065043713806143223346176887807399261
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_344 :
Polynomial.coeff recurrence2Scalar1Shift 344 = -((179569143 * 10 ^ 70 + 3173593376308425053197375554586639614401408933532306127922230829277761) * 10 ^ 70 + 6406561874302069445889866544832602400030487847986859721352203448241924)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_345 :
Polynomial.coeff recurrence2Scalar1Shift 345 = -((1708535 * 10 ^ 70 + 1743522740883014070913567075488058175347889302808445697420056413037661) * 10 ^ 70 + 1324215931882979547090228930881597003100521933999054924765167078766131)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_346 :
Polynomial.coeff recurrence2Scalar1Shift 346 = (92444 * 10 ^ 70 + 6669534726633547829850470866495659734920542887191534925919166949037140) * 10 ^ 70 + 9184945980906752289745131304256416485697338113829949905019343523703264
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_347 :
Polynomial.coeff recurrence2Scalar1Shift 347 = -((990 * 10 ^ 70 + 2066509625702748765708311092496981512300474443960105483787329325278246) * 10 ^ 70 + 3444398744317570228554529951234224872874154269893117560265883242148180)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_348 :
Polynomial.coeff recurrence2Scalar1Shift 348 = -((5 * 10 ^ 70 + 5242634405650158448748017937691377566969271432871242994077996758122811) * 10 ^ 70 + 9722416758391216742991487705441055703735258407952351217796538015556345)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_349 :
Polynomial.coeff recurrence2Scalar1Shift 349 = 1916439582804041872507907060249973275028772091291694956978085438104714 * 10 ^ 70 + 4363352567553237593224661360188406543189070745709218943220728783027080
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_350 :
Polynomial.coeff recurrence2Scalar1Shift 350 = -(7258288941569823104429136929581691237668776771902019673167427507687 * 10 ^ 70 + 5729302101774980314407122125952644722030429944185661105584690817676300)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_351 :
Polynomial.coeff recurrence2Scalar1Shift 351 = -(123280384993621711288762244692711051902388581468071630272932776955 * 10 ^ 70 + 2809922305793172153223614163350625582223605322574063103142661967946801)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_352 :
Polynomial.coeff recurrence2Scalar1Shift 352 = 951168892397358558758716363206423832467134757033378854335661897 * 10 ^ 70 + 8880753663912525961259307218444506191474101790711845250114101220120436
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_353 :
Polynomial.coeff recurrence2Scalar1Shift 353 = 3467629762002353561443122587079327958431555063401258111511686 * 10 ^ 70 + 3809384068241754510296866048624743385272507032044200600099195996809594
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_354 :
Polynomial.coeff recurrence2Scalar1Shift 354 = -(45349067005314714322359656823785546087004198249592269570456 * 10 ^ 70 + 1069581225714825634508458417130295731099765253232934288135825856554663)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_355 :
Polynomial.coeff recurrence2Scalar1Shift 355 = -(26097969624679803860543307695089476148297768889600281031 * 10 ^ 70 + 186482823539842039138437843868256020379175291193845936229721524789348)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_356 :
Polynomial.coeff recurrence2Scalar1Shift 356 = 1131388678700372124052737313280042735214179809708032046 * 10 ^ 70 + 5281662394943847120837840835591870650720284269067216207624116852678689
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_357 :
Polynomial.coeff recurrence2Scalar1Shift 357 = -(982542722637315907089102478021536984614513090698500 * 10 ^ 70 + 8637949377823524159316720746229199300357714483444306213238577247218368)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_358 :
Polynomial.coeff recurrence2Scalar1Shift 358 = -(15547062724423495378782920342959903681011896791291 * 10 ^ 70 + 3103470134695179590103488813640570480851764393745914137484766151217236)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_359 :
Polynomial.coeff recurrence2Scalar1Shift 359 = 29613538457672325996471272342638017130582372956 * 10 ^ 70 + 9127014118870628379682414071307624750315954246899169709396342393479351
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_360 :
Polynomial.coeff recurrence2Scalar1Shift 360 = 106982705301376935468094419388446830910647276 * 10 ^ 70 + 3432774217401311833111862561469521179485389123948762268546426932553265
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_361 :
Polynomial.coeff recurrence2Scalar1Shift 361 = -(336720367803295822608178644346700730549158 * 10 ^ 70 + 5879106383819782913656553638407334088500526024213892065588883284097645)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_362 :
Polynomial.coeff recurrence2Scalar1Shift 362 = -(184327924866978663682147130818675925217 * 10 ^ 70 + 6442599354119733223133615192100024356981891397847782676740531053635691)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_363 :
Polynomial.coeff recurrence2Scalar1Shift 363 = 1637124497575280288357994529924489822 * 10 ^ 70 + 8872089643986686717164560907081603185764886812058332119006933932017982
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_364 :
Polynomial.coeff recurrence2Scalar1Shift 364 = -(1434158984376313720315010517494169 * 10 ^ 70 + 1601658158825684142173095408596128699018916608350860877895569431256498)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_365 :
Polynomial.coeff recurrence2Scalar1Shift 365 = -(1905295551668522094867155611078 * 10 ^ 70 + 657565929298310819865309143527959092393635108341642520098275737214001)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_366 :
Polynomial.coeff recurrence2Scalar1Shift 366 = 4303054418452796514757305006 * 10 ^ 70 + 8538117826378881921255579611320810185757450113311148179258291119860124
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_367 :
Polynomial.coeff recurrence2Scalar1Shift 367 = -(2617093558235847539819486 * 10 ^ 70 + 4239009338799570592344638457461055897488761109931109780247434538351467)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_368 :
Polynomial.coeff recurrence2Scalar1Shift 368 = 21410664907156726302 * 10 ^ 70 + 132190291438455220513080607121445611773376103587469621689132071372722
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_369 :
Polynomial.coeff recurrence2Scalar1Shift 369 = 601275027250547330 * 10 ^ 70 + 3935430784215275429574416090328544096456236918420282048691376629590324
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_370 :
Polynomial.coeff recurrence2Scalar1Shift 370 = -(237556003902084 * 10 ^ 70 + 5222624684785817797678869863860761127955146080635713093293766456236739)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_371 :
Polynomial.coeff recurrence2Scalar1Shift 371 = 32411342942 * 10 ^ 70 + 6129005497628942927412559044635481475161936312002721236952992559160306
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_372 :
Polynomial.coeff recurrence2Scalar1Shift 372 = -(666421 * 10 ^ 70 + 9067112409026817356407962596311646849614520723125563865679367303092943)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_373 :
Polynomial.coeff recurrence2Scalar1Shift 373 = -(163 * 10 ^ 70 + 8247426752605123269079746683954617437412558333969026391882408662628674)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_374 :
Polynomial.coeff recurrence2Scalar1Shift 374 = 105175662714001782261935149484042874977134648584263254546421996061775
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_375 :
Polynomial.coeff recurrence2Scalar1Shift 375 = -1878369461119149595505357420861111799888220854844044514029306268
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_376 :
Polynomial.coeff recurrence2Scalar1Shift 376 = 8379617675549280037784306732183268668629035211673311546995
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_377 :
Polynomial.coeff recurrence2Scalar1Shift 377 = 19516506400240705591384137467204049919784225072076051
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_378 :
Polynomial.coeff recurrence2Scalar1Shift 378 = -91779007694975403946065398805950810314968314574
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_379 :
Polynomial.coeff recurrence2Scalar1Shift 379 = 60951273568382323836751524600664864680464
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Shift_coeff_380 :
Polynomial.coeff recurrence2Scalar1Shift 380 = -3360009522262143161703435836062336