audit-session036b-axioms.txt
11 declarations audited · 3 standard axioms only · updated 08-24-2026
Raw #print axioms transcript
'NguyenRH1.logDeriv_riemannZeta_sub_nearZeros_le_tight' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.pinch_tight_R' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.C0hat_le_of_ten_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.pinchF_at_critical' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.pinchF'_at_critical' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_twelve_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_twelve_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_three_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_four_thirds_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.neg_log_one_sub_le_four' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_two_point_five_zero_two_four_le' depends on axioms: [propext, Classical.choice, Quot.sound]