gamma_lt_two_thirds
plain-language theorem explainer
The Euler-Mascheroni constant satisfies γ < 2/3. Researchers bounding γ for use in renormalization group flows or Mertens theorems would cite this result to close the interval (1/2, 2/3). The proof is a one-line term that invokes the corresponding Mathlib inequality on the abbrev gamma.
Claim. $γ < 2/3$, where $γ := lim_{n→∞} (H_n - ln n)$ is the Euler-Mascheroni constant.
background
In the Recognition Science module on constants, γ is introduced via the abbrev gamma := Real.eulerMascheroniConstant, defined as the limit of harmonic numbers minus the logarithm. The module C-011 records that numerical bounds are established while first-principles derivation from the ledger-zeta structure remains blocked on the Riemann hypothesis (M-001). Upstream, gamma_pos already shows γ > 1/2; the present result supplies the matching upper bound.
proof idea
The proof is a term-mode one-liner that directly applies the Mathlib lemma Real.eulerMascheroniConstant_lt_two_thirds to the local definition of gamma.
why it matters
This bound is consumed by euler_mascheroni_bounds to obtain the closed interval 0 < γ < 1, completing the numerical side of registry item C-011. Within the RS framework it supports the constants section where γ enters QFT renormalization and prime-counting formulas, though the full derivation path stays open pending ledger-zeta development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.