`or`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.EulerMascheroni
domain: Constants
line: 16 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.EulerMascheroni on GitHub at line 16.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  13**STARTED** — γ is formalized with proved bounds; RS first-principles
  14derivation remains blocked on the ledger–zeta development.
  15Dependency: M-001 (Riemann hypothesis). Potential RS path: ledger harmonic
  16structure or zeta zeros; not yet developed.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Constants
  21namespace EulerMascheroni
  22
  23open Real
  24
  25/-! ## Definition and Bounds (from Mathlib) -/
  26
  27/-- γ = Euler-Mascheroni constant = lim_{n→∞} (H_n - ln n) ≈ 0.5772. -/
  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:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.