Documentation

MazurTorsion.Kubert.OrderSevenBacktrackingResultantRecurrence2LookupScalar1ExceptionalPart0.Coefficients0To90

Recurrence 2 lookup certificate: Scalar1Exceptional coefficient convolution #

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_41 :
Polynomial.coeff recurrence2Scalar1Exceptional 41 = 1216252520168463779020 * 10 ^ 70 + 6815235423152429033680972094052863077809961236129408639578112232815689
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_42 :
Polynomial.coeff recurrence2Scalar1Exceptional 42 = -(26101510780030752265592 * 10 ^ 70 + 8537523810087481878112379419557665929329268445204818570012173333582046)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_43 :
Polynomial.coeff recurrence2Scalar1Exceptional 43 = 614721023706610279294045 * 10 ^ 70 + 8168513574786470309325218445009409867543021659152099403452162662752815
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_44 :
Polynomial.coeff recurrence2Scalar1Exceptional 44 = -(16978660438227732910202577 * 10 ^ 70 + 3529905552676407421260361172110450110570736022250570817217349694466713)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_45 :
Polynomial.coeff recurrence2Scalar1Exceptional 45 = 499031990155345803470981694 * 10 ^ 70 + 8283724014863632135061123226627886630418698359206301923822544825311101
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_46 :
Polynomial.coeff recurrence2Scalar1Exceptional 46 = -(14171520678745432069474834616 * 10 ^ 70 + 6237166731562480926031868314479696125659748586081296701735941683233815)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_47 :
Polynomial.coeff recurrence2Scalar1Exceptional 47 = 378133667819017897292688860852 * 10 ^ 70 + 2716991620559971382829375369303019189984845575646812838024057447197583
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_48 :
Polynomial.coeff recurrence2Scalar1Exceptional 48 = -(9524973844178613184534706157726 * 10 ^ 70 + 2424884412460628913622697745127591617393579902292902515307135134276890)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_49 :
Polynomial.coeff recurrence2Scalar1Exceptional 49 = 228001798822185432154042586504111 * 10 ^ 70 + 4580704437745288454386839069603018550256167757028140879018272538147798
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_50 :
Polynomial.coeff recurrence2Scalar1Exceptional 50 = -(5186794630279306705885008950038123 * 10 ^ 70 + 1154509298386988221335751612735471402662412335706679841411661776131323)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_51 :
Polynomial.coeff recurrence2Scalar1Exceptional 51 = 111826916223877443533904804934580981 * 10 ^ 70 + 2688709462168759052404840003369755891074551184679959660638706465473324
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_52 :
Polynomial.coeff recurrence2Scalar1Exceptional 52 = -(2283353608063386857041068403320428327 * 10 ^ 70 + 1483527067959367933596588145383015466559966952263804273598192399489816)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_53 :
Polynomial.coeff recurrence2Scalar1Exceptional 53 = 44266955120877671291851838589532162547 * 10 ^ 70 + 8879905740909747093466084351607753987992561649686683823680134272386516
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_54 :
Polynomial.coeff recurrence2Scalar1Exceptional 54 = -(818086436949256656634218121264175924116 * 10 ^ 70 + 4009887324747322259116565477395955793733643872169687551614714987607337)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_55 :
Polynomial.coeff recurrence2Scalar1Exceptional 55 = 14458678675984193625872871847351022101884 * 10 ^ 70 + 2900719049570472798183921783482711163433072414069460109985012437496036
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_56 :
Polynomial.coeff recurrence2Scalar1Exceptional 56 = -(244747021797543437718232939530114134887154 * 10 ^ 70 + 3754303101108673359500424271230347691219722121716973395669692080569893)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_57 :
Polynomial.coeff recurrence2Scalar1Exceptional 57 = 3969079651082537423835777635798712858700060 * 10 ^ 70 + 5284694727967565652907752437379906304403622467351608056957113495683477
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_58 :
Polynomial.coeff recurrence2Scalar1Exceptional 58 = -(61672633293259774097044757802600906746841244 * 10 ^ 70 + 8716656960888520356898610950329781340353588526134864133038983050350919)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_59 :
Polynomial.coeff recurrence2Scalar1Exceptional 59 = 918673117727671021259440778990301799487290329 * 10 ^ 70 + 922859694523121769217440850222174385160665738238582339729217625352105
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_60 :
Polynomial.coeff recurrence2Scalar1Exceptional 60 = -(13131089672175718568495860199063844749718900369 * 10 ^ 70 + 990149494685329265098233884703330263118389273510748851910837603992474)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_61 :
Polynomial.coeff recurrence2Scalar1Exceptional 61 = 180273740407332335750003291762218731713942533467 * 10 ^ 70 + 785555834061966126314525453698345097958658752219521780971381114316685
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_62 :
Polynomial.coeff recurrence2Scalar1Exceptional 62 = -(2378971173702196255471348304330207112811004260892 * 10 ^ 70 + 8651397366326667523588156580665239461478784568493717299977014015889644)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_63 :
Polynomial.coeff recurrence2Scalar1Exceptional 63 = 30194820566545114266694089345919514094105550494675 * 10 ^ 70 + 9426391713583901803679397480497765668394666410640234864877534692399134
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_64 :
Polynomial.coeff recurrence2Scalar1Exceptional 64 = -(368831000550788613037548172692801806310620273939103 * 10 ^ 70 + 1264834120955521154919674890313431521682129120581319989456194508311249)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_65 :
Polynomial.coeff recurrence2Scalar1Exceptional 65 = 4338951217422435937079746436002554931123935923689662 * 10 ^ 70 + 4038091747903485316328107511851892227456531189148513420596363386313513
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_66 :
Polynomial.coeff recurrence2Scalar1Exceptional 66 = -(49196720831130206192537739382485117657767136357520494 * 10 ^ 70 + 3549907254469330655901149702079442268921591786623988425290413690769164)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_67 :
Polynomial.coeff recurrence2Scalar1Exceptional 67 = 537998674414972518260589222028769904071850181415012870 * 10 ^ 70 + 2581212885965290589005424495156762528980356973203938691265617712889637
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_68 :
Polynomial.coeff recurrence2Scalar1Exceptional 68 = -(5677584450413388126853750539563042455579896542351258655 * 10 ^ 70 + 8192477492514246137413742610739463246079122491890731172746389930890566)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_69 :
Polynomial.coeff recurrence2Scalar1Exceptional 69 = 57848967366960347912956346474459736311390861168228717067 * 10 ^ 70 + 710985715156732721213921590397964649988427829266596783227934888047522
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_70 :
Polynomial.coeff recurrence2Scalar1Exceptional 70 = -(569378425550393155909903954906557904019659818613316321247 * 10 ^ 70 + 164027301475147904801290182962870712404276931653356846089717753641238)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_71 :
Polynomial.coeff recurrence2Scalar1Exceptional 71 = 5416679751423633448205882624220586435775898958538766289513 * 10 ^ 70 + 5478027406806500711085309627608990093193427087097885007342021057130770
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_72 :
Polynomial.coeff recurrence2Scalar1Exceptional 72 = -(49837284931864100659340365906043915869624340221955596874020 * 10 ^ 70 + 9554884299644790176251284594418266444770152416844526320401616298646521)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_73 :
Polynomial.coeff recurrence2Scalar1Exceptional 73 = 443712417847931999593864058328707808888776346614691015509273 * 10 ^ 70 + 7181658175555393943413420931306839451288817754976430377723595521499570
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_74 :
Polynomial.coeff recurrence2Scalar1Exceptional 74 = -(3824496054691671787124854989472719182109621630952789722771649 * 10 ^ 70 + 3189219438557276909678345456592950746052631853093587661159947759650438)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_75 :
Polynomial.coeff recurrence2Scalar1Exceptional 75 = 31926765523701269978274031713114220166350491172951547489556358 * 10 ^ 70 + 3635934695872926667967907119378315314608111783784188879027103125305498
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_76 :
Polynomial.coeff recurrence2Scalar1Exceptional 76 = -(258249551810161798654690498648346719943260399266106273687766944 * 10 ^ 70 + 2504668429827309281523974698992243437968282579298295042371844463420273)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_77 :
Polynomial.coeff recurrence2Scalar1Exceptional 77 = 2025089614881399953651733417135666851087346696724295665950348139 * 10 ^ 70 + 287289802820870236371238728469196974558762810470377909498399563453990
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_78 :
Polynomial.coeff recurrence2Scalar1Exceptional 78 = -(15402160416589051839066324667032125350393527419889483595041326289 * 10 ^ 70 + 3348788638758407543719792151733633775559002788462220562274200966193041)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_79 :
Polynomial.coeff recurrence2Scalar1Exceptional 79 = 113666595488369591795583557054228636696730032422753871210080883601 * 10 ^ 70 + 3112405774176498793032609786534955338885091449994932744537696486121748
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_80 :
Polynomial.coeff recurrence2Scalar1Exceptional 80 = -(814230130938314344428166480752598110835028386571996691938344719220 * 10 ^ 70 + 9451144660518861888951494579047821488081193383868308603440875263089897)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_81 :
Polynomial.coeff recurrence2Scalar1Exceptional 81 = 5663358890258287219968292821189530415348768211786130275166877643269 * 10 ^ 70 + 3059402210547036623536625016006304188380301546167818684445500559476680
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_82 :
Polynomial.coeff recurrence2Scalar1Exceptional 82 = -(38264378425755540935185068301386497571321033693208218240842344780614 * 10 ^ 70 + 9147483925379668328373793466876344970272142338286637536130957448231804)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_83 :
Polynomial.coeff recurrence2Scalar1Exceptional 83 = 251254782389540004620511943060919867542490929555836195236689040135291 * 10 ^ 70 + 195240724419585255196986765860667463184159619279555899648947691058600
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_84 :
Polynomial.coeff recurrence2Scalar1Exceptional 84 = -(1604046085809259812966633320135083176241050246776300113857498020719115 * 10 ^ 70 + 427741046136714567941828075027120024836996532310077073498024929751437)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_85 :
Polynomial.coeff recurrence2Scalar1Exceptional 85 = 9959229885516701526552553825394348958717701469241334556533585214332532 * 10 ^ 70 + 1887619530813552146248121509309357538374678517433543543295891931458784
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_86 :
Polynomial.coeff recurrence2Scalar1Exceptional 86 = -((6 * 10 ^ 70 + 148366341236769233528335069123182210169356687833532809633887919809182) * 10 ^ 70 + 1686428270623181169721020529506289666914529514951356183492407950865923)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_87 :
Polynomial.coeff recurrence2Scalar1Exceptional 87 = (35 * 10 ^ 70 + 3447485318825047948098284239147276181687972765060166578279365060657668) * 10 ^ 70 + 3495603201625649925981112511581479182324787306698190407660613530249686
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_88 :
Polynomial.coeff recurrence2Scalar1Exceptional 88 = -((202 * 10 ^ 70 + 1744901467896522213094286757386774984711033161287712536757572408451764) * 10 ^ 70 + 8945873813625624629590397722929747549706544435515052868213147554499155)
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_89 :
Polynomial.coeff recurrence2Scalar1Exceptional 89 = (1126 * 10 ^ 70 + 3373339771028264931050312785453921578155915020753783667251781095607765) * 10 ^ 70 + 4060133921851318189818912170898334620964022347307277294332377185705966
theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_90 :
Polynomial.coeff recurrence2Scalar1Exceptional 90 = -((6113 * 10 ^ 70 + 8530101188062737430105749977731680175629219835067276436323351591108501) * 10 ^ 70 + 9363256101086415841449829931237024546761235454270126608166313606139381)