audit-session036-axioms.txt
22 declarations audited · 3 standard axioms only · updated 08-24-2026
Raw #print axioms transcript
'NguyenRH1.far_series_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.farG_main_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.farGRight_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.farGLeft_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.farG_tail_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.farG_summable' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.farW_tsum_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.zeroMult_conj' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.analyticOrderAt_riemannZeta_conj' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.iteratedDeriv_riemannZeta_conj' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.C0hat_two_mul_add_one_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.C0hat_add_one_le_of_fourteen_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.C0hat_two_t_add_one_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.tail11_inv_sq_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.tail11_log_div_sq_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.tail11_loglog_div_sq_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.tail14_inv_add_sq_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.tail14_log_div_add_sq_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.tail14_loglog_div_add_sq_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_ten_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_one_add_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.neg_log_one_sub_le' depends on axioms: [propext, Classical.choice, Quot.sound]