audit-session029-axioms.txt
30 declarations audited · 3 standard axioms only · updated 08-23-2026
Raw #print axioms transcript
'NguyenRH1.Fexpr' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.badPoint' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.analyticAt_digamma' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.analyticAt_digamma_div_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.zeta_zero_classification' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_zeta_sub_mult_div_eventually' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_zeta_eq_logDeriv_zetaA_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Fexpr_eventually_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digammaSeriesPart' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.add_nat_add_one_ne_zero_of_mem_ball' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digammaSeriesPart_analyticOn' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digamma_eq_seriesPart_near_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Fexpr_eventually_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.riemannZeta_neg_two_mul' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.integerComplement_of_mem_ball_neg_natCast' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.add_nat_add_one_ne_zero_of_mem_ball_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digammaSeriesPartSub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digammaSeriesPartSub_analyticOn' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digammaSeriesPart_eq_sub_add_single' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Hsub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digamma_eq_neg_inv_add_Hsub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Hsub_analyticAt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Fexpr_eventually_neg_two_mul' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Fexpr_eventually_nontrivial' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Fexpr_analyticAt_of_not_bad' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exists_ball_good_of_not_bad' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Gentire' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gentire_eq_Fexpr' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gentire_eventually_eq_witness' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gentire_analyticAt_and_eq' depends on axioms: [propext, Classical.choice, Quot.sound]