gamma_pos
plain-language theorem explainer
The declaration proves that the Euler-Mascheroni constant γ is positive. Researchers assembling constant registries for renormalization or zeta-regularized quantities in physics cite this when confirming sign properties inside the C-011 item. The proof is a one-line term that chains a numerical fact 0 < 1/2 through an order-transitivity lemma to the Mathlib inequality 1/2 < γ.
Claim. Let γ denote the Euler-Mascheroni constant. Then 0 < γ.
background
The Euler-Mascheroni module registers γ as the limit lim (H_n − ln n) and places it under registry item C-011. The module states that γ appears in QFT renormalization, Mertens prime-counting formulas, and the Riemann zeta function, while noting that a first-principles RS derivation is blocked pending ledger-zeta work and the Riemann hypothesis (M-001).
proof idea
The proof is a term-mode application of the transitivity lemma lt_trans to the pair (0 < 1/2) verified by norm_num and the Mathlib fact 1/2 < Real.eulerMascheroniConstant.
why it matters
The result supplies the lower bound inside the parent theorem euler_mascheroni_bounds that packages 0 < γ < 1 and thereby supports the C-011 claim that γ is well-defined with proved bounds. It sits inside the broader constants layer of the Recognition Science framework, where numerical positivity is recorded while full derivation from the forcing chain or RCL remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.