audit-session038d-axioms.txt

Raw #print axioms transcript

'NguyenRH1.sf_abs_le_rectInt_add_zeroSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.zeroSum_norm_le_four_FAlt_add_one' depends on axioms: [propext, Classical.choice, Quot.sound]
def NguyenRH1.ZeroCountGlobalProp : Prop :=
∀ (T : ℝ), 2 ≤ T → ∑ ρ ∈ ⋯.toFinset, ↑(Zeta23.zeroMult ρ) ≤ FAlt T
def NguyenRH1.MZeroProp : Prop :=
∀ (t : ℝ), |t| ≤ 10 → ‖logDeriv riemannZeta (-5 / 2 + ↑t * Complex.I)‖ ≤ 1.3352
'NguyenRH1.exists_zero_avoiding_T_wide' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.zeroWindowWide_card_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.zeroWindowWide_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.zeroGlobalWindow_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.zeroBothWindow_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.zeroGlobalWindowNeg_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.zeroTerm_norm_le_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.zeroSum_nontriv_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.zeroBothWindow_sum_eq_two_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.trivTerm_norm_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]