audit-session041-axioms.txt
29 declarations audited · 3 standard axioms only · updated 08-26-2026
Raw #print axioms transcript
'NguyenRH1.Z2hat_mono' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.nearZerosSub_mult_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.continuousAt_logDeriv_zeta' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.continuousOn_logDeriv_zeta' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Jlag_norm_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.zeta_ne_zero_left_vertical' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.zeta_ne_zero_horizontal' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.rectangleIntegral_Jlag_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.VIntegral_norm' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.HIntegral_split' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.jlag_left_vertical_norm_even' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Z2hat_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.vIntegral_Jlag_left_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.kFun_right_vertical_norm_le_exp_sqrt_add_third' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.vIntegral_Jlag_right_le_exp_third_IIMaj' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.integral_one_div_sqrt_sq_add_sq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.arcsinh_right_endpoint_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.arcsinh_left_endpoint_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.per_zero_integral_le_two_log' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hIntegral_Jlag_mid_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hIntegral_Jlag_mid_neg_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hIntegral_Jlag_full_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hIntegral_Jlag_full_neg_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hIntegral_Jlag_full_two_sides' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.C0hat_le_self' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.pinch_horizontal' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sfBoundProp' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.lambda_pos_finite_height_closed' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.lambda_pos_finite_height_verified' depends on axioms: [propext, Classical.choice, Quot.sound]