gamma
plain-language theorem explainer
gamma registers the Euler-Mascheroni constant as the standard limit of the harmonic numbers minus the logarithm inside the Recognition Science constants registry. Researchers working on C-011 bounds for device modulation or lattice symmetries cite it when anchoring numerical values. The declaration is a direct noncomputable alias to Mathlib's Real.eulerMascheroniConstant with no reduction steps.
Claim. Define the Euler-Mascheroni constant by $gamma = lim_{n to infty} (H_n - ln n)$ where $H_n$ is the nth harmonic number and the limit equals approximately 0.57721.
background
The Constants.EulerMascheroni module implements registry item C-011. It formalizes gamma approximately 0.5772 with proved bounds while noting that a first-principles Recognition Science derivation remains blocked on ledger-zeta development and depends on the Riemann hypothesis labeled M-001.
proof idea
This is a direct abbreviation that aliases Mathlib's Real.eulerMascheroniConstant. No lemmas or tactics are invoked beyond the alias assignment.
why it matters
The definition supplies the numerical anchor for gamma in downstream modules such as PhotobiomodulationDevice.phi_fifth_in_alpha_band and Chemistry.CrystalSymmetry lattice constraints. It advances the C-011 registry item by providing a formalized constant with bounds while leaving open the RS-native derivation via ledger harmonic structure or zeta zeros, currently dependent on the Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.