euler_mascheroni_implies_pos
plain-language theorem explainer
The theorem extracts the strict positivity of the Euler-Mascheroni constant γ from the hypothesis that 0 < γ < 1. Researchers auditing the C-011 registry item would cite it when chaining bound results inside the constants module. The proof is a direct term projection that returns the left conjunct of the input pair.
Claim. If $0 < γ < 1$ where $γ$ is the Euler-Mascheroni constant, then $0 < γ$.
background
The module formalizes the Euler-Mascheroni constant γ ≈ 0.5772 under registry item C-011, with proved bounds but first-principles derivation still blocked on ledger-zeta development and the Riemann hypothesis. The constant is introduced as the noncomputable abbrev γ := Real.eulerMascheroniConstant, equivalently the limit lim (H_n - ln n), and an upstream sibling already records γ > 1/2. The local setting is the constants domain of Recognition Science, where numerical bounds on γ are collected before any RS-native derivation from the phi-ladder or forcing chain.
proof idea
The proof is a one-line term wrapper that projects the first component of the hypothesis conjunction, returning the left inequality 0 < gamma directly from the input pair.
why it matters
It supplies the positivity step required by the immediate downstream theorem euler_mascheroni_implies_ne_zero, which concludes gamma ≠ 0 from the same bound bundle. The result sits inside the C-011 formalization of bounds for γ and contributes to the broader Recognition Science program of placing constants on the phi-ladder (T5 J-uniqueness, T6 phi fixed point, T8 D = 3). The open question it touches is the still-missing first-principles derivation of γ itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.