audit-session024-axioms.txt
32 declarations audited · 3 standard axioms only · updated 08-22-2026
Raw #print axioms transcript
'NguyenRH1.scaledZeta_jensen_count' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_scaledZeta_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.scaledZeta_order_ne_top' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.one_le_analyticOrderNatAt_scaledZeta' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.scaledZeroFinset_sum_order_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.scaledZeroFinset_card_le_sum' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exists_collection_radius' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.collRadius_gap' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.rC_gap' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.collZeros_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Cf_eq_div_collProd' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Cf_eq_zeroFactor_div' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Cf_collZeros_analytic' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Cf_collZeros_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Cf_collZeros_log_norm_zero_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Cf_collZeros_norm_le_sphere' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Cf_collZeros_norm_le_ball' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_9_4_le_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_33_32_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.two_le_log_abs_t' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.jensen_bound_elementary' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.card96_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.collMultSum_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_50_card_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Mbound_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.mem_nearZeros' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.affMap_injOn' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.zeroMult_affMap' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sum_image_zeroMult_div' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.nearZeros_subset_image' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sum_image_zeroMult_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logDeriv_riemannZeta_sub_nearZeros_le' depends on axioms: [propext, Classical.choice, Quot.sound]