Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar4LeftPart1.Coefficients333To370

Recurrence 2 lookup certificate: Scalar4Left 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.recurrence2Scalar4Left_coeff_333 :
Polynomial.coeff recurrence2Scalar4Left 333 = (2307200295 * 10 ^ 70 + 2410068588526326006574281093429914745742949468344731314484222586057972) * 10 ^ 70 + 7516653819397739717159969583959054452291245647364303913887672172864578
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_334 :
Polynomial.coeff recurrence2Scalar4Left 334 = (11406779 * 10 ^ 70 + 7977066865725637719379164138778711087086525398412089732320360626346660) * 10 ^ 70 + 3818127033790555374724894452406338025097448395704818080118990405459644
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_335 :
Polynomial.coeff recurrence2Scalar4Left 335 = -((697529 * 10 ^ 70 + 3213654010781350442015070493227407690282154431912935224762277674424471) * 10 ^ 70 + 1283795487845982504514989493788090360652702255814523227074424432471142)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_336 :
Polynomial.coeff recurrence2Scalar4Left 336 = (6489 * 10 ^ 70 + 2194718333609136129448788673428856769152615860860738719774596061748963) * 10 ^ 70 + 7155905909862141325307470687091049936906738933834928646021456804723601
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_337 :
Polynomial.coeff recurrence2Scalar4Left 337 = (30 * 10 ^ 70 + 8695956020992005932122005377853457708957783818165594230193232137299571) * 10 ^ 70 + 8700715701398547562687447911227796439848832102172512370523168934989256
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_338 :
Polynomial.coeff recurrence2Scalar4Left 338 = -(8779348054274603868633145231399673446067205880383942468834372576709277 * 10 ^ 70 + 1064379239339237659283484983898335062450648290534330816996557791541294)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_339 :
Polynomial.coeff recurrence2Scalar4Left 339 = 22955668251681367426145905197663604333827758026661663372557529741659 * 10 ^ 70 + 8413803072556336109690596194738194758113561598349812525749814372892787
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_340 :
Polynomial.coeff recurrence2Scalar4Left 340 = 451205516432624245144089292001180267403980024210481934697578413937 * 10 ^ 70 + 1194300541407776757236916014573355802253163867765307309354310394487147
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_341 :
Polynomial.coeff recurrence2Scalar4Left 341 = -(2542894913007301020701314721333677527237989691178452281002035164 * 10 ^ 70 + 6162220078896615272427592523973448159394815142482423402839225567075320)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_342 :
Polynomial.coeff recurrence2Scalar4Left 342 = -(10988828153302358162403987621629646646016865285514650623689875 * 10 ^ 70 + 7690525311830400207697001697587720312233964717753381928768750101929962)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_343 :
Polynomial.coeff recurrence2Scalar4Left 343 = 98055518779167923266149144022162615188482069400461423208488 * 10 ^ 70 + 8479536918385240633556967272005585408658551019119708559944415845493512
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_344 :
Polynomial.coeff recurrence2Scalar4Left 344 = 96769249965179101270761599000022351481521468640005049348 * 10 ^ 70 + 4518756232153567088371005425145583540744849612762288591866637567535703
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_345 :
Polynomial.coeff recurrence2Scalar4Left 345 = -(1955641074457363387749366771712497634599367431955375486 * 10 ^ 70 + 3408329480034770397721329046893309405024951778942440061709145941324513)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_346 :
Polynomial.coeff recurrence2Scalar4Left 346 = 1198088326700605842301397698263800066746866523334781 * 10 ^ 70 + 9749727199740527674941271028639751519285496071716724016588182981298374
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_347 :
Polynomial.coeff recurrence2Scalar4Left 347 = 20898965597171765418892035126505357047423905269136 * 10 ^ 70 + 3545682764335627144048628343718025453376037775647926158093287186585945
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_348 :
Polynomial.coeff recurrence2Scalar4Left 348 = -(36927054572406245824113192611148392393005301168 * 10 ^ 70 + 4238228672524826086475970842419150622709904710125191118504004751529485)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_349 :
Polynomial.coeff recurrence2Scalar4Left 349 = -(101343972339495147504736121222518343196575980 * 10 ^ 70 + 1156465877566377839719642365589198268763252504814246159980917594861652)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_350 :
Polynomial.coeff recurrence2Scalar4Left 350 = 329909628281391012385526555648870364719958 * 10 ^ 70 + 9755692321672338224641128595003340977101045836405474836932802730324175
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_351 :
Polynomial.coeff recurrence2Scalar4Left 351 = 5751550178138790206911370276275792501 * 10 ^ 70 + 202986116771797396340413569271029833160692439835547880222874555032902
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_352 :
Polynomial.coeff recurrence2Scalar4Left 352 = -(1043519172428822362656435514431173813 * 10 ^ 70 + 1757960725571978378296505045391478767553460712065827581639371861336181)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_353 :
Polynomial.coeff recurrence2Scalar4Left 353 = 1316680062178650020029106419020533 * 10 ^ 70 + 2305414969476690816165184367224445019470211676591368591119816015626822
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_354 :
Polynomial.coeff recurrence2Scalar4Left 354 = -(48270186663555403852497780756 * 10 ^ 70 + 3301077132350384613266143975212790468785997983711509445615432079704506)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_355 :
Polynomial.coeff recurrence2Scalar4Left 355 = -(1074103843081017538596661454 * 10 ^ 70 + 2063600805540997636775599733818546927307761718203045293756417439614933)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_356 :
Polynomial.coeff recurrence2Scalar4Left 356 = 860819746184293824550618 * 10 ^ 70 + 7078198756540823143077168321786851354000740510003229482239886863228355
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_357 :
Polynomial.coeff recurrence2Scalar4Left 357 = -(237958476481220329239 * 10 ^ 70 + 7192629457847024489549595656329426627342737853846350861427195212674414)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_358 :
Polynomial.coeff recurrence2Scalar4Left 358 = -(3052362917741937 * 10 ^ 70 + 963551315671427182257773063370697163139049721462965460973033327536436)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_359 :
Polynomial.coeff recurrence2Scalar4Left 359 = 12766462012605 * 10 ^ 70 + 9592602868324623424629251105327371201453831875477226921928305523840648
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_360 :
Polynomial.coeff recurrence2Scalar4Left 360 = -(2099185717 * 10 ^ 70 + 2280374352788343565022700267859861812173291148739924942918011101126552)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_361 :
Polynomial.coeff recurrence2Scalar4Left 361 = 111508 * 10 ^ 70 + 6002945738303457601383928800539082657728636135282724862934248567723281
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_362 :
Polynomial.coeff recurrence2Scalar4Left 362 = -9296179741274619959460766959955767250849995999223238035917850610073356
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_363 :
Polynomial.coeff recurrence2Scalar4Left 363 = -677021628558179902893303453097705817617237491363398540243187099140
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_364 :
Polynomial.coeff recurrence2Scalar4Left 364 = 12204675399264991471266989721795493250007052652520874129046480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_365 :
Polynomial.coeff recurrence2Scalar4Left 365 = -59668864105667124966617425590913911253139770347105500288
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_366 :
Polynomial.coeff recurrence2Scalar4Left 366 = 45778506313975631848233270436100395922506125530922
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_367 :
Polynomial.coeff recurrence2Scalar4Left 367 = 16610979903556272851696298142152348112049976
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_368 :
Polynomial.coeff recurrence2Scalar4Left 368 = -17110468348557752567808013608801134123
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_369 :
Polynomial.coeff recurrence2Scalar4Left 369 = 231959337222114242015213921853
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar4Left_coeff_370 :
Polynomial.coeff recurrence2Scalar4Left 370 = -791494537845229613466