Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar3ExceptionalPart1.Coefficients335To375

Recurrence 2 lookup certificate: Scalar3Exceptional 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.recurrence2Scalar3Exceptional_coeff_335 :
Polynomial.coeff recurrence2Scalar3Exceptional 335 = (2558 * 10 ^ 70 + 5333609156069619124659147382472567121236660661218392648846612823418517) * 10 ^ 70 + 9748666710032208250446504259659781753268774893879825414040894979581601
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_336 :
Polynomial.coeff recurrence2Scalar3Exceptional 336 = -((80 * 10 ^ 70 + 1757258233696569605485324792993035411043520129541714179945099019610221) * 10 ^ 70 + 4963386628685288419783235883340070813422104460056120298344515837872215)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_337 :
Polynomial.coeff recurrence2Scalar3Exceptional 337 = -((12 * 10 ^ 70 + 7346499732764452483108839994726661914160653054797039945415870240905574) * 10 ^ 70 + 5754639562355583445692924972738183135124549134731515529339304761978749)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_338 :
Polynomial.coeff recurrence2Scalar3Exceptional 338 = -(2840189895340002962312746131548153954972940200572156687726696131045608 * 10 ^ 70 + 6972656973582448965771357006156982975679233914212473854132635300594979)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_339 :
Polynomial.coeff recurrence2Scalar3Exceptional 339 = 240326590842088190744578907375669803312619161600262258499296570402389 * 10 ^ 70 + 57565387402109072372214171884906346187894868415192207073033301987310
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_340 :
Polynomial.coeff recurrence2Scalar3Exceptional 340 = 22248407190491508971513859902761638533367316536316684451879218505915 * 10 ^ 70 + 3843517676138750458632720623692090488978914003643718326785928752311998
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_341 :
Polynomial.coeff recurrence2Scalar3Exceptional 341 = 958593598828548150057401159793470577815469425535528720012714664797 * 10 ^ 70 + 2171447808323868222610513168726171399559674832823894498389200358644417
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_342 :
Polynomial.coeff recurrence2Scalar3Exceptional 342 = 27198416126871994525131420649331751570751756717507597178600027784 * 10 ^ 70 + 9531075680260545215723472048706721915379112401714471216764966009144587
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_343 :
Polynomial.coeff recurrence2Scalar3Exceptional 343 = 557916738887624504655523819001995629033654732013706818013994895 * 10 ^ 70 + 3901712702859659706095720251185865606915682204850366608808300761243793
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_344 :
Polynomial.coeff recurrence2Scalar3Exceptional 344 = 8605456358572908073356457387622534918375739204468673486693789 * 10 ^ 70 + 5242983968532527473871386028945245476139548796750580981776087780942226
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_345 :
Polynomial.coeff recurrence2Scalar3Exceptional 345 = 101612434929577365977223212731873264037907440617901787695374 * 10 ^ 70 + 867813162583111586053268106880109540384138681016492058161947685017677
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_346 :
Polynomial.coeff recurrence2Scalar3Exceptional 346 = 923570904691216235005924573453807784047384235122772543447 * 10 ^ 70 + 9216402445229540010244160585013700406155764363758671682639956321657535
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_347 :
Polynomial.coeff recurrence2Scalar3Exceptional 347 = 6426764575193164454625256914389724958905175090136482915 * 10 ^ 70 + 8792926389589612812543493223653593117069305833406035161331356662422647
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_348 :
Polynomial.coeff recurrence2Scalar3Exceptional 348 = 33552681580011259217427356470536537432330841638060674 * 10 ^ 70 + 1028629124774477337159827497278740332989366635046177260323986330031612
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_349 :
Polynomial.coeff recurrence2Scalar3Exceptional 349 = 124903954485799370129506294144337366778360057259805 * 10 ^ 70 + 6691574903377265239325749628831294599550179414836604923560552903251761
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_350 :
Polynomial.coeff recurrence2Scalar3Exceptional 350 = 284467443988108052740201559015193693062115610310 * 10 ^ 70 + 6376762842436432844671691044210246498913724337662786540732050552924913
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_351 :
Polynomial.coeff recurrence2Scalar3Exceptional 351 = 96919329309575115810363266522407302331545213 * 10 ^ 70 + 2312851464262507535853743944339175065469211680096033228784024728808055
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_352 :
Polynomial.coeff recurrence2Scalar3Exceptional 352 = -(1907997367312922042608726897106117592033684 * 10 ^ 70 + 6114086830331997199725491548882764479926003578277373605483362425682620)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_353 :
Polynomial.coeff recurrence2Scalar3Exceptional 353 = -(7106454853494958141238177927955034222765 * 10 ^ 70 + 7274676712152151911145410350243746025415209371401942583715799653363650)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_354 :
Polynomial.coeff recurrence2Scalar3Exceptional 354 = -(10424474607868737328921212849089691116 * 10 ^ 70 + 9790647676228808475345944975039489685927105423249219348568390331875525)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_355 :
Polynomial.coeff recurrence2Scalar3Exceptional 355 = 4940439777968443037030153383344809 * 10 ^ 70 + 7915828551603944280790637060256514769655078196668834085506387978165824
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_356 :
Polynomial.coeff recurrence2Scalar3Exceptional 356 = 48297956634529289014665888790364 * 10 ^ 70 + 4876671688425523392760270891281002962400178943745755924034595607791063
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_357 :
Polynomial.coeff recurrence2Scalar3Exceptional 357 = 81129653760573399311333001261 * 10 ^ 70 + 3113372952868521827594539801035263665257596273640105686575439882835632
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_358 :
Polynomial.coeff recurrence2Scalar3Exceptional 358 = 34333195538514120053093030 * 10 ^ 70 + 6846552690021819296732933142354123575575680057861819925231014031992371
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_359 :
Polynomial.coeff recurrence2Scalar3Exceptional 359 = -(86655218248311165663849 * 10 ^ 70 + 971808851767326104265813945969265719595165839736754458484933041666531)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_360 :
Polynomial.coeff recurrence2Scalar3Exceptional 360 = -(172908079401735005663 * 10 ^ 70 + 1457197213112020936634632755076519751514725627191116913877389628694130)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_361 :
Polynomial.coeff recurrence2Scalar3Exceptional 361 = -(153082333270124634 * 10 ^ 70 + 2250509333767950467862510423401599178092354787603795010513861845663014)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_362 :
Polynomial.coeff recurrence2Scalar3Exceptional 362 = -(78691694018128 * 10 ^ 70 + 8455751709903878040925708229393823141112825237976829858435676791226815)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_363 :
Polynomial.coeff recurrence2Scalar3Exceptional 363 = -(24551936777 * 10 ^ 70 + 8465120289327752543933855826758355937263890317880191113094818533263217)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_364 :
Polynomial.coeff recurrence2Scalar3Exceptional 364 = -(4607328 * 10 ^ 70 + 5300993054559788516292117597967019935296321196107596911654359100711592)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_365 :
Polynomial.coeff recurrence2Scalar3Exceptional 365 = -(505 * 10 ^ 70 + 4878857782894039382841266157355483153263516127269833803255046094114382)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_366 :
Polynomial.coeff recurrence2Scalar3Exceptional 366 = -314360548704161721232711598665403869432812482847758332073976232516527
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_367 :
Polynomial.coeff recurrence2Scalar3Exceptional 367 = -10410397204066192364460051365504577706061046438508635194153972870
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_368 :
Polynomial.coeff recurrence2Scalar3Exceptional 368 = -162282759350867435952606765182298523381676141578943905061015
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_369 :
Polynomial.coeff recurrence2Scalar3Exceptional 369 = -1068873158294425762268180727250779896172024106199360369
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_370 :
Polynomial.coeff recurrence2Scalar3Exceptional 370 = -3165235645754014046010262867403287390685644340487
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_371 :
Polynomial.coeff recurrence2Scalar3Exceptional 371 = -3818780553013805840581005380943155647737877
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_372 :
Polynomial.coeff recurrence2Scalar3Exceptional 372 = -991462750806985695491116848863711095
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_373 :
Polynomial.coeff recurrence2Scalar3Exceptional 373 = -10602472227767369736371076242
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_374 :
Polynomial.coeff recurrence2Scalar3Exceptional 374 = -26247306779745334905
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar3Exceptional_coeff_375 :
Polynomial.coeff recurrence2Scalar3Exceptional 375 = -18890099430