audit-session025-axioms.txt
26 declarations audited · 3 standard axioms only · updated 08-23-2026
Raw #print axioms transcript
'NguyenRH1.norm_le_abs_re_add_abs_im'' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.im_div_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.re_div_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Gammaℝ_ne_zero_of_im_ne_zero'' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.differentiableAt_Gammaℝ_of_im_ne_zero'' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_congr' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gammaR_shift_four' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gammaR_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_Gammaℝ_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.completedZeta_eventuallyEq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_completedZeta_eq_add' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_completedZeta_neg_one_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.riemannZeta_one_sub_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_zeta_fe' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.riemannZeta_one_sub_eq_zero_of_nontrivial' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.one_sub_mem_nearZeros_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.mem_nearZeros_of_one_sub_mem_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.nearZeros_neg_eq_image' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.zeroMult_one_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sum_nearZeros_neg_reflect' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_log_le_of_one_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_digamma_le_log_of' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gammaR_bracket_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digamma_add_natCast' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_digamma_sub_log_le_of_two_le_abs_im' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_riemannZeta_sub_nearZeros_le_left' depends on axioms: [propext, Classical.choice, Quot.sound]