Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence4LookupScalar0ExceptionalPart0.Coefficients0To39

Recurrence 4 lookup certificate: Scalar0Exceptional coefficient convolution #

This is a checked coefficient-lookup shard for the fourth pseudo-division recurrence in the order-seven certificate.

source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_0 :
Polynomial.coeff recurrence4Scalar0Exceptional 0 = 0
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_1 :
Polynomial.coeff recurrence4Scalar0Exceptional 1 = -520207759061720837503698646314245381652480
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_2 :
Polynomial.coeff recurrence4Scalar0Exceptional 2 = -80176542757117106762179335791982722411384832
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_3 :
Polynomial.coeff recurrence4Scalar0Exceptional 3 = 7961147542114361054198652697380472650249405126144
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_4 :
Polynomial.coeff recurrence4Scalar0Exceptional 4 = -12801194048176919542111208667830225225028952357272512
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_5 :
Polynomial.coeff recurrence4Scalar0Exceptional 5 = -5520403742575209328650660587654629536331870853915396544
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_6 :
Polynomial.coeff recurrence4Scalar0Exceptional 6 = 33530218742111736651421207990495574509455974168370039199120
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_7 :
Polynomial.coeff recurrence4Scalar0Exceptional 7 = -50199140861999302147275019955366394763475201792088084165846432
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_8 :
Polynomial.coeff recurrence4Scalar0Exceptional 8 = 26514014125175591585847043581688762618568900223235024741260478128
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_9 :
Polynomial.coeff recurrence4Scalar0Exceptional 9 = 38078434605379574503690368753091197852505409235973521824433340358288
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_10 :
Polynomial.coeff recurrence4Scalar0Exceptional 10 = -(7 * 10 ^ 70 + 8088378031705371418900235995026675380881422563199849231252590033139404)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_11 :
Polynomial.coeff recurrence4Scalar0Exceptional 11 = 5889 * 10 ^ 70 + 7590974963725579656367875526549456456417606980729726296870141325907372
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_12 :
Polynomial.coeff recurrence4Scalar0Exceptional 12 = -(1867539 * 10 ^ 70 + 2879740424231012241855419224200156981258868587951461576389814211313404)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_13 :
Polynomial.coeff recurrence4Scalar0Exceptional 13 = -(381161618 * 10 ^ 70 + 4073194077384950599684051376179751211805845382607313557055410729404252)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_14 :
Polynomial.coeff recurrence4Scalar0Exceptional 14 = 682788897301 * 10 ^ 70 + 7256503094986888669003509766355207939527316868446153739773097347506700
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_15 :
Polynomial.coeff recurrence4Scalar0Exceptional 15 = -(351393870647453 * 10 ^ 70 + 9731086702925604070396315386998651738576175110177623566247188279685979)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_16 :
Polynomial.coeff recurrence4Scalar0Exceptional 16 = 107351713221657427 * 10 ^ 70 + 6791535953583532252222833335777432987538157416510590889059539883377356
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_17 :
Polynomial.coeff recurrence4Scalar0Exceptional 17 = -(21152975201580741871 * 10 ^ 70 + 5814413149391047597812881034011418207508091282804225203184509557239954)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_18 :
Polynomial.coeff recurrence4Scalar0Exceptional 18 = 2763658319666791215866 * 10 ^ 70 + 505470502987526204821592027221924650250444710353239113750519708458024
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_19 :
Polynomial.coeff recurrence4Scalar0Exceptional 19 = -(435600652392651983545068 * 10 ^ 70 + 1231427253586183897503899490209229936263324109676094043975284478192051)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_20 :
Polynomial.coeff recurrence4Scalar0Exceptional 20 = 206548350768903331309212392 * 10 ^ 70 + 1540405068086424849641222053720812534040004973765836898078274257708408
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_21 :
Polynomial.coeff recurrence4Scalar0Exceptional 21 = -(98756117069683014351829614771 * 10 ^ 70 + 4652716636665620078771253917969533505863432497185873739913974264137868)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_22 :
Polynomial.coeff recurrence4Scalar0Exceptional 22 = 34540428351588007439799560400830 * 10 ^ 70 + 4565933162273888186926005429663181548059227097989813910375075864615717
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_23 :
Polynomial.coeff recurrence4Scalar0Exceptional 23 = -(9438920235686930112885462199844789 * 10 ^ 70 + 6117270026551532148116822382131761282521867823790160420977373026027136)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_24 :
Polynomial.coeff recurrence4Scalar0Exceptional 24 = 2153288870762470831329941345106312292 * 10 ^ 70 + 3085715737107917926510752902377602021320668666822484905035332168767689
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_25 :
Polynomial.coeff recurrence4Scalar0Exceptional 25 = -(436223623285231518760921764692154270836 * 10 ^ 70 + 1235014854461778983534287337401935237387029216188977989745802552548425)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_26 :
Polynomial.coeff recurrence4Scalar0Exceptional 26 = 85308589667264456296586121640632088598884 * 10 ^ 70 + 1722717205059666015790729762084669652993052791899557007433725880767302
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_27 :
Polynomial.coeff recurrence4Scalar0Exceptional 27 = -(17864212162385331807100530429318875157818467 * 10 ^ 70 + 3283890167782426384799810941226317898482693615806379191793766138297223)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_28 :
Polynomial.coeff recurrence4Scalar0Exceptional 28 = 4216484542978621509166777994940112718759735888 * 10 ^ 70 + 2294223562647749604649028120019752731554972206464968465200835196129576
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_29 :
Polynomial.coeff recurrence4Scalar0Exceptional 29 = -(1065068941892500341353103726367076112096551000644 * 10 ^ 70 + 882197606846034690695071686687109022605781378461883331404172922766948)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_30 :
Polynomial.coeff recurrence4Scalar0Exceptional 30 = 264891751482229119342980745841791758126832759908554 * 10 ^ 70 + 9287536256857217037211552328557206757728444370818568023708990457933809
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_31 :
Polynomial.coeff recurrence4Scalar0Exceptional 31 = -(61671945333902239425216298430576299217682844338557292 * 10 ^ 70 + 1059082308721783497459510537646976140912087143172215027308962945497609)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_32 :
Polynomial.coeff recurrence4Scalar0Exceptional 32 = 13193424409608397521643211985922134701596282123832087685 * 10 ^ 70 + 940504341718331289283167590140660497867383068786505732287713362339040
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_33 :
Polynomial.coeff recurrence4Scalar0Exceptional 33 = -(2585334375682443882452108021140869923494642384845197120343 * 10 ^ 70 + 7062822890168270781409448429452878240331058129682807028382060403126172)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_34 :
Polynomial.coeff recurrence4Scalar0Exceptional 34 = 465191423219745058396978941301826754598551312441439111247721 * 10 ^ 70 + 3012880261249524398842066415079375136277838332391686190790776392888427
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_35 :
Polynomial.coeff recurrence4Scalar0Exceptional 35 = -(77162201276148448092476666530483850562306014855252513403936333 * 10 ^ 70 + 4587997893295084603846624871916951664945041167617786699263657340784056)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_36 :
Polynomial.coeff recurrence4Scalar0Exceptional 36 = 11845125820841697184480625823314288148460571398183830938961646839 * 10 ^ 70 + 5737356756341130057565928563678682852855818171196995738263581012591045
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_37 :
Polynomial.coeff recurrence4Scalar0Exceptional 37 = -(1688735341369468278219145111751542790942885963645757019385538129571 * 10 ^ 70 + 5303962892000046369429198217584784601085316740475152078947039207746922)
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_38 :
Polynomial.coeff recurrence4Scalar0Exceptional 38 = 224281521827640109383663902111286772731220405225302316452270274376065 * 10 ^ 70 + 5348208267165183107536418196800062562222964419258318163227418837037896
source
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence4Scalar0Exceptional_coeff_39 :
Polynomial.coeff recurrence4Scalar0Exceptional 39 = -((2 * 10 ^ 70 + 7821665225734128729565739333494579504811007389273236996895746104913617) * 10 ^ 70 + 7526918627345612431375257452061433861304886753639630383970078626040770)