euler_mascheroni_bounds
plain-language theorem explainer
The theorem establishes that the Euler-Mascheroni constant γ satisfies 0 < γ < 1. Researchers working on constants in the Recognition Science framework cite this when bounding γ for renormalization or Mertens-type estimates. The proof is a term-mode construction that pairs the positivity result with a numerical tightening of the 2/3 upper bound to 1.
Claim. Let γ denote the Euler-Mascheroni constant, defined as the limit of H_n − ln n as n tends to infinity. Then 0 < γ < 1.
background
The module formalizes the Euler-Mascheroni constant γ ≈ 0.5772 under registry item C-011. It records appearances in QFT renormalization, prime-counting via Mertens theorems, and the Riemann zeta function. The RS first-principles derivation remains blocked on M-001 (Riemann hypothesis) and the undeveloped ledger–zeta connection, per the module doc-comment.
proof idea
The term proof constructs the conjunction directly as ⟨gamma_pos, lt_of_lt_of_le gamma_lt_two_thirds (by norm_num)⟩. It invokes the upstream positivity lemma (γ > 1/2) and applies a numerical comparison to strengthen the 2/3 bound to a strict inequality below 1.
why it matters
This supplies the proved bound bundle for C-011 in the constants registry. It confirms γ is well-defined within the formalization but leaves the full RS derivation open, pending ledger–zeta development and M-001. The result sits downstream of the gamma positivity and 2/3 lemmas and supports later work on physical constants inside the phi-ladder and ledger structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.