euler_mascheroni_bounds
The declaration proves that the Euler-Mascheroni constant satisfies 0 < γ < 1. Researchers in quantum field theory renormalization or analytic number theory studying the zeta function would cite these bounds. The proof is a term-mode pair that combines the positivity lemma with a numerical tightening of the 2/3 upper bound to 1.
claim$0 < γ < 1$, where $γ = lim_{n→∞} (H_n - ln n)$ is the Euler-Mascheroni constant.
background
The module formalizes the RS framework for the Euler-Mascheroni constant γ ≈ 0.5772 under registry item C-011. γ is introduced as the limit of harmonic numbers minus the natural logarithm and appears in renormalization, Mertens theorems, and the Riemann zeta function. Upstream results supply gamma_pos (γ > 1/2) and gamma_lt_two_thirds (γ < 2/3), both drawn from Mathlib bounds on the constant. The local setting records that a first-principles RS derivation remains blocked on ledger-zeta development and M-001 (Riemann hypothesis).
proof idea
The proof is a term-mode construction that returns the pair consisting of gamma_pos together with the result of lt_of_lt_of_le applied to gamma_lt_two_thirds and the norm_num fact that 2/3 < 1.
why it matters in Recognition Science
This bound supports the C-011 status by confirming γ lies inside (0,1) and thereby closes a basic well-definedness check in the constants module. It sits downstream from the gamma positivity and upper-bound lemmas. The framework treats γ as a constant appearing in QFT and prime-counting contexts, yet full derivation from the forcing chain or RCL remains open pending ledger-zeta connection and resolution of M-001.
scope and limits
- Does not derive γ from the J-cost or phi-ladder structures.
- Does not prove irrationality or any deeper arithmetic property of γ.
- Does not resolve the ledger-zeta connection or the Riemann hypothesis dependency.
- Does not supply a numerical value or optimal bounds beyond the (0,1) interval.
formal statement (Lean)
53theorem euler_mascheroni_bounds : 0 < gamma ∧ gamma < 1 :=
proof body
Term-mode proof.
54 ⟨gamma_pos, lt_of_lt_of_le gamma_lt_two_thirds (by norm_num)⟩
55
56/-- Euler-Mascheroni bound bundle implies positivity of `γ`. -/