audit-session040-axioms.txt
41 declarations audited · 3 standard axioms only · updated 08-26-2026
Raw #print axioms transcript
'NguyenRH1.Jlag_differentiableAt_dogleg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.holomorphicOn_Jlag_dogleg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.rectangleIntegral_Jlag_dogleg_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.rectangleIntegral'_Jlag_dogleg_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.upper_right_horizontal_eq_dogleg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.kFun_conj' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Jlag_conj' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.kFun_three_add_it_norm_le_exp_five_halves_add_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_term_vonMangoldt_three_le_half' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.dirichletC3_le_half' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_logDeriv_zeta_le_dirichletC3' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_logDeriv_zeta_le_half' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.vIntegral_Jlag_three_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_term_vonMangoldt_le_two_pow' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_logDeriv_zeta_le_two_pow' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.one_add_div_pow_norm_le_exp_four_ninths' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Jlag_dogleg_norm_le_envelope' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.integral_exp_neg_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.cdog_gt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exp_four_thirds_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hIntegral_Jlag_dogleg_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.kFun_right_vertical_norm_le_exp_sqrt_half_add_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.vIntegral_Jlag_right_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hIntegral_Jlag_low_le_dogLegUpper' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hIntegral_Jlag_low_neg_norm_le_dogLegUpper' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.dogLegUpper_two_sides' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_logDeriv_zeta_le_dirichletCX' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_term_vonMangoldt_X_le_three_pow' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.dirichletCX_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_nine_quarters_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_four_ninths_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.four_ninths_rpow_sqrt_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.three_pow_neg_two_sqrt_sub_two_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_logDeriv_zeta_le_iimZeta' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.vIntegral_Jlag_right_norm_le_quarter' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.vIntegral_Jlag_right_le_IIMaj_quarter' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.marginTilde_convex' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.marginTilde_FAlt_80000_pos' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.marginTilde_FAlt_80000_lt_100000' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.lambda_pos_finite_height_verified' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exp_five_halves_le' depends on axioms: [propext, Classical.choice, Quot.sound]