gamma_numerical_bounds
plain-language theorem explainer
The declaration establishes that the Euler-Mascheroni constant γ satisfies 1/2 < γ < 2/3. Researchers formalizing constants inside the Recognition Science framework cite the result to fix the numerical interval for γ in registry item C-011. The proof is a one-line term construction that pairs two standard inequalities on the Euler-Mascheroni constant taken from the real-numbers library.
Claim. Let γ denote the Euler-Mascheroni constant. Then 1/2 < γ < 2/3.
background
Module C-011 registers the Euler-Mascheroni constant γ ≈ 0.5772 inside the Recognition Science framework. γ is introduced via the classical limit definition lim (H_n − ln n) as n → ∞, where H_n is the nth harmonic number. The module states that numerical bounds are now proved while a first-principles RS derivation remains blocked on the Riemann hypothesis (M-001) and the undeveloped ledger–zeta connection.
proof idea
The proof is a term-mode construction. It directly assembles the conjunction by supplying the two library facts one_half_lt_eulerMascheroniConstant and eulerMascheroniConstant_lt_two_thirds.
why it matters
The result supplies the proved numerical bounds required by registry item C-011. It anchors γ for later constant work in the framework, where γ enters renormalization, Mertens theorems, and the zeta function. Full placement inside the forcing chain (T0–T8) and the Recognition Composition Law is deferred until the ledger–zeta link and M-001 are resolved. The declaration therefore closes the bounds subtask while leaving the derivation path open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.