gamma_pos

formal source

  28noncomputable abbrev gamma : ℝ := Real.eulerMascheroniConstant
  29
  30/-- γ is positive (γ > 1/2). -/
  31theorem gamma_pos : 0 < gamma :=
  32  lt_trans (by norm_num : (0 : ℝ) < 1/2) Real.one_half_lt_eulerMascheroniConstant
  33
  34/-- γ < 2/3 (Mathlib bound). -/
  35theorem gamma_lt_two_thirds : gamma < 2/3 :=
  36  Real.eulerMascheroniConstant_lt_two_thirds
  37
  38/-- Numerical bounds: 1/2 < γ < 2/3. -/
  39theorem gamma_numerical_bounds : (1/2 : ℝ) < gamma ∧ gamma < 2/3 :=
  40  ⟨Real.one_half_lt_eulerMascheroniConstant, Real.eulerMascheroniConstant_lt_two_thirds⟩
  41
  42/-! ## C-011 Status -/
  43
  44/-- **C-011 Status**: γ is well-defined; RS derivation OPEN.
  45
  46    γ appears in:
  47    - Renormalization (QFT)
  48    - Prime counting (Mertens)
  49    - Riemann zeta ζ(s)
  50
  51    Full derivation from RS: BLOCKED on M-001 (Riemann hypothesis)
  52    and development of ledger–zeta connection. -/
  53theorem euler_mascheroni_bounds : 0 < gamma ∧ gamma < 1 :=
  54  ⟨gamma_pos, lt_of_lt_of_le gamma_lt_two_thirds (by norm_num)⟩
  55
  56/-- Euler-Mascheroni bound bundle implies positivity of `γ`. -/
  57theorem euler_mascheroni_implies_pos (h : 0 < gamma ∧ gamma < 1) :
  58    0 < gamma :=
  59  h.1
  60
  61/-- Euler-Mascheroni bound bundle excludes `γ = 0`. -/