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_16 :
Polynomial.coeff recurrence2Scalar1Exceptional 16 = -23486103977331997213656684522659317171297991239
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_17 :
Polynomial.coeff recurrence2Scalar1Exceptional 17 = 8861209744903959524227084045421552323329367415932
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_18 :
Polynomial.coeff recurrence2Scalar1Exceptional 18 = -1835837107160486887844105836901275743180585842981902
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_19 :
Polynomial.coeff recurrence2Scalar1Exceptional 19 = 278281263234306252637888166202118400629637805544257180
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_20 :
Polynomial.coeff recurrence2Scalar1Exceptional 20 = -31401932830928446492272214302630988825076492741864915483
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_21 :
Polynomial.coeff recurrence2Scalar1Exceptional 21 = 2230098768090490842098879078213809834770314790511247789349
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_22 :
Polynomial.coeff recurrence2Scalar1Exceptional 22 = -14097112821477161082448798351778589167834044534453940534742
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_23 :
Polynomial.coeff recurrence2Scalar1Exceptional 23 = -20372432399045333015224669477371498287944951777075646459553565
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_24 :
Polynomial.coeff recurrence2Scalar1Exceptional 24 = 3087079387097708558362688667462151545104618947698177111302936082
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_25 :
Polynomial.coeff recurrence2Scalar1Exceptional 25 = -264115857803296722468857332995045938193834819190733799174560745097
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_26 :
Polynomial.coeff recurrence2Scalar1Exceptional 26 = 13254390370493159238773594781690424630270609869184890709558694704316
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_27 :
Polynomial.coeff recurrence2Scalar1Exceptional 27 = -84414838998069269064649135833245185665155515795552398977390758728751
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_28 :
Polynomial.coeff recurrence2Scalar1Exceptional 28 = -(5 * 10 ^ 70 + 4735955506111689550638620245393688467551022869545529039944029442430925)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_29 :
Polynomial.coeff recurrence2Scalar1Exceptional 29 = 609 * 10 ^ 70 + 2933466514809983097142506571516271520144979690044985945028218627506701
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_30 :
Polynomial.coeff recurrence2Scalar1Exceptional 30 = -(40961 * 10 ^ 70 + 4657605696150481697137900191155757586545091744831338791765869573602271)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_31 :
Polynomial.coeff recurrence2Scalar1Exceptional 31 = 2005638 * 10 ^ 70 + 5820653320370801894525169788308071160825570829952735520212496608431857
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_32 :
Polynomial.coeff recurrence2Scalar1Exceptional 32 = -(74550574 * 10 ^ 70 + 9294192734512668865917394411531073864649882934042087150951780241564914)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_33 :
Polynomial.coeff recurrence2Scalar1Exceptional 33 = 2097442510 * 10 ^ 70 + 4042359252252418863069276041855199693896077193281865189073140697283640
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_34 :
Polynomial.coeff recurrence2Scalar1Exceptional 34 = -(43875577601 * 10 ^ 70 + 2969895418005257364515496588600659514459681081245540600264826229111736)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_35 :
Polynomial.coeff recurrence2Scalar1Exceptional 35 = 755074331180 * 10 ^ 70 + 29928053191187719245600299794327068975307310843077341538858075074610
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_36 :
Polynomial.coeff recurrence2Scalar1Exceptional 36 = -(21109007477762 * 10 ^ 70 + 111283971264158904408138453045001696208607938805519709064377230409330)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_37 :
Polynomial.coeff recurrence2Scalar1Exceptional 37 = 1124245757151181 * 10 ^ 70 + 9930004418404780212262739850816496535933786341175534364071841275791945
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_38 :
Polynomial.coeff recurrence2Scalar1Exceptional 38 = -(53354890403191954 * 10 ^ 70 + 8372048813855759131529736583183821812686755290401134300139210761558626)
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_39 :
Polynomial.coeff recurrence2Scalar1Exceptional 39 = 1903483954854730421 * 10 ^ 70 + 2388498795263929587473788807570197989246518403049548376702788821299616
theorem
MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar1Exceptional_coeff_40 :
Polynomial.coeff recurrence2Scalar1Exceptional 40 = -(52803214684650867620 * 10 ^ 70 + 9665816131027035352534108024947430208767367404068413962137461034653200)
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)