Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3LeftPart1.Coefficients337To374

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.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_337 :
Polynomial.coeff recurrence2Scalar3Left 337 = (1713412113 * 10 ^ 70 + 2380170548139694638702910527328266194385444866262321257907713242943324) * 10 ^ 70 + 1176578964398111909832111373453225374233292318941362434491374556004473
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_338 :
Polynomial.coeff recurrence2Scalar3Left 338 = (2830769 * 10 ^ 70 + 3204197992827768762447652568029224727183642082762927369940402906073459) * 10 ^ 70 + 5347004513188700170839093724472724652078635037619166044986399959381779
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_339 :
Polynomial.coeff recurrence2Scalar3Left 339 = -((423224 * 10 ^ 70 + 3619611735297800503461487013000196057934378448975250645850042328361734) * 10 ^ 70 + 2862663821259137379082165324372427701850404846722047483080130726350540)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_340 :
Polynomial.coeff recurrence2Scalar3Left 340 = (4600 * 10 ^ 70 + 7011527543347161581512729318554051989650382928325655747115905070466506) * 10 ^ 70 + 9811886634516903482399473854853856596579341180770689403235222781887118
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_341 :
Polynomial.coeff recurrence2Scalar3Left 341 = (11 * 10 ^ 70 + 8304126432707249631195155017327352625264606472194104576412265482521704) * 10 ^ 70 + 5920128949330098077949732051185503280004230574531108515388209491262757
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_342 :
Polynomial.coeff recurrence2Scalar3Left 342 = -(5405837252171348042979984183340999502644009082701875918709057825296547 * 10 ^ 70 + 4714278453950929310708905943729938927844759644496409026290024486766840)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_343 :
Polynomial.coeff recurrence2Scalar3Left 343 = 19738513681865029371806025083338685527731129477019435220950292866652 * 10 ^ 70 + 2782591823317053660619477001870636207040662627702903656048164357206995
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_344 :
Polynomial.coeff recurrence2Scalar3Left 344 = 248752319861657634491590027160208225404930745796658523890791681871 * 10 ^ 70 + 297116908409518092170981606274481296163435209241249928644790665475297
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_345 :
Polynomial.coeff recurrence2Scalar3Left 345 = -(1723920327064793341056660867294972846011007182122515942892057768 * 10 ^ 70 + 1374317909948923902298579048839467486363673220655862397466089562351464)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_346 :
Polynomial.coeff recurrence2Scalar3Left 346 = -(5088454320232556029484271482919170587038036499858951675855533 * 10 ^ 70 + 6876379295228149411906500253180207331651255946786124587931067162727316)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_347 :
Polynomial.coeff recurrence2Scalar3Left 347 = 60829493402318203930589243795817633336875492242596277454790 * 10 ^ 70 + 1812905255037096034999435992086991095542260333613045930374043919862726
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_348 :
Polynomial.coeff recurrence2Scalar3Left 348 = 16238836400748776325926586579350938327505718238027781887 * 10 ^ 70 + 8153419721209160483045359014146297946649206033695820350985702362045845
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_349 :
Polynomial.coeff recurrence2Scalar3Left 349 = -(1128215886770036836912455109308525500590182993664748125 * 10 ^ 70 + 7842322474704604551151887025506198322523132259789780587706408001164676)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_350 :
Polynomial.coeff recurrence2Scalar3Left 350 = 1295076570859286081552224863333775937444769359461597 * 10 ^ 70 + 3427301611495838354690533251702382179651347740965243978760592746831993
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_351 :
Polynomial.coeff recurrence2Scalar3Left 351 = 11004841822322302368302871260521898405192552565524 * 10 ^ 70 + 493738334654212575138164189170273463331396220676231252119589794400570
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_352 :
Polynomial.coeff recurrence2Scalar3Left 352 = -(25427159667199743460741496963082870124331345052 * 10 ^ 70 + 7058021020249893838727978428014520095871206801079234391386913849611504)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_353 :
Polynomial.coeff recurrence2Scalar3Left 353 = -(43736786144096067401321081860530861199169085 * 10 ^ 70 + 2007184910360237826283753177684185516841987137798045954103565034117775)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_354 :
Polynomial.coeff recurrence2Scalar3Left 354 = 192050527178511654926347789943707017487536 * 10 ^ 70 + 3130755792309929484597401350143872703656456515627652767513105720199103
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_355 :
Polynomial.coeff recurrence2Scalar3Left 355 = -(68100958374523921820822546928838047823 * 10 ^ 70 + 8558091592471827353905107802238178606566727110652939772158280986330628)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_356 :
Polynomial.coeff recurrence2Scalar3Left 356 = -(499531830966420261029331335531570896 * 10 ^ 70 + 7934384823400964888651419790183774432626495282453070965227052907098196)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_357 :
Polynomial.coeff recurrence2Scalar3Left 357 = 791047997498558552571917798559726 * 10 ^ 70 + 9249192091405279765699677116162123108867295392231128005886037608390571
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_358 :
Polynomial.coeff recurrence2Scalar3Left 358 = -(248452242912370909206071832202 * 10 ^ 70 + 9672440219885300245896774930179462670673983075801130612468305981432545)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_359 :
Polynomial.coeff recurrence2Scalar3Left 359 = -(388293726068666152816049677 * 10 ^ 70 + 8418052244824442813621652295495081539833126932337847431126844504775235)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_360 :
Polynomial.coeff recurrence2Scalar3Left 360 = 404397741696115078246667 * 10 ^ 70 + 7913941072483337550811594821878005252062236656863367558357015302452374
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_361 :
Polynomial.coeff recurrence2Scalar3Left 361 = -(140475978139930382982 * 10 ^ 70 + 7888807441890036080978230430467841539741556673033100691253781423032345)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_362 :
Polynomial.coeff recurrence2Scalar3Left 362 = 12351359454808699 * 10 ^ 70 + 3578226148894827097326566064895119289089816936186691413164145351153783
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_363 :
Polynomial.coeff recurrence2Scalar3Left 363 = 3160881795291 * 10 ^ 70 + 3581448363262346312735596755610485598424394185273730368799612913819151
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_364 :
Polynomial.coeff recurrence2Scalar3Left 364 = -(732774502 * 10 ^ 70 + 8586495626094457694580250091407758313113403185049071760062253720554657)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_365 :
Polynomial.coeff recurrence2Scalar3Left 365 = 47762 * 10 ^ 70 + 808211605104521592343781990483756619150576160789972041968293854581033
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_366 :
Polynomial.coeff recurrence2Scalar3Left 366 = -9454948867434608337668196268082805373340226918649820558566057715237343
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_367 :
Polynomial.coeff recurrence2Scalar3Left 367 = -65868902530199323065629140195009959460502941916682889267898432408
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_368 :
Polynomial.coeff recurrence2Scalar3Left 368 = 2443822343223082194782832322743060621912073396130668310433814
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_369 :
Polynomial.coeff recurrence2Scalar3Left 369 = -14202745730161737235415289213336709812151430136454293417
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_370 :
Polynomial.coeff recurrence2Scalar3Left 370 = 15742905152230615934102356088409185682380339195076
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_371 :
Polynomial.coeff recurrence2Scalar3Left 371 = -2995791125347133595513127658029915158440732
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_372 :
Polynomial.coeff recurrence2Scalar3Left 372 = -1410347095972451960882153638879833503
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_373 :
Polynomial.coeff recurrence2Scalar3Left 373 = 19718337189424179550878922270
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Left_coeff_374 :
Polynomial.coeff recurrence2Scalar3Left 374 = -67965145443184571654