audit-session033-axioms.txt
14 declarations audited · 3 standard axioms only · updated 08-24-2026
Raw #print axioms transcript
'NguyenRH1.differentiableAt_Gammaℝ_of_not_neg_nat' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_Gammaℝ_eq_of_not_neg_nat' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gapCircle_sep' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.nearZeros_count_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gapCircle_sep_of_mem_nearZeros' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digamma_right_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digamma_circle_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_one_div_le_of_norm_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_one_div_sub_one_le_of_norm_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_pi_le_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_logPi_div_two_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.dirichletC2_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_circle_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Fexpr_circle_le' depends on axioms: [propext, Classical.choice, Quot.sound]