euler_mascheroni_implies_ne_zero
plain-language theorem explainer
The result shows that the Euler-Mascheroni constant γ satisfies γ ≠ 0 under the hypothesis 0 < γ < 1. Workers on Recognition Science constants would cite it to exclude the zero solution inside the C-011 bound bundle. The proof is a one-line wrapper that extracts positivity from the same bounds and converts the strict inequality to nonzero.
Claim. If $0 < γ < 1$, then $γ ≠ 0$, where $γ$ is the Euler-Mascheroni constant defined by $γ = lim_{n→∞} (H_n - ln n)$.
background
Module C-011 registers γ as the limit of the difference between the harmonic numbers and the natural logarithm. The bound hypothesis 0 < γ < 1 is supplied by sibling results that place γ inside (0,1). Upstream, euler_mascheroni_implies_pos extracts the left half of the conjunction to give 0 < γ directly from the same hypothesis pair.
proof idea
One-line wrapper that applies euler_mascheroni_implies_pos to the input hypothesis, then feeds the resulting strict inequality into ne_of_gt.
why it matters
The declaration finishes the zero-exclusion half of the C-011 bound bundle. It supports the registry question on γ's physical role by guaranteeing the constant is nonzero, consistent with its appearance in harmonic and zeta contexts. The module records that a full Recognition Science derivation of γ itself remains blocked on ledger-zeta development and the Riemann hypothesis dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.