or
plain-language theorem explainer
The structure or in Constants.EulerMascheroni bundles Euler-Mascheroni constant aspects into the Recognition Science constants registry. Number theorists and physicists linking zeta functions to physical constants would cite it when tracing gamma bounds. It is introduced as a plain structure definition with no proof steps or lemmas.
Claim. Let $C$ be the structure bundling the Euler-Mascheroni constant $γ = lim_{n→∞}(H_n - ln n) ≈ 0.5772$ together with related bounds and positivity statements, where $H_n$ denotes the $n$th harmonic number.
background
The module formalizes the RS framework for the Euler-Mascheroni constant γ ≈ 0.5772 under registry item C-011. It sits inside the broader Constants domain and imports the abstract CPM constants bundle (Knet, Cproj, Ceng, Cdisp with nonnegativity) from LawOfExistence.Constants together with the from theorem that extracts seven axioms into four structural conditions. Upstream also supplies the and theorem from CirclePhaseLift that produces an explicit log-derivative bound M, the zeta abbrev from ArithmeticFunctions, and the constant scalar field definition.
proof idea
The declaration is a structure definition (def_or_abbrev style) that directly assembles fields from the imported constants bundle and zeta function without applying any lemmas or tactics.
why it matters
It populates the C-011 registry item whose RS derivation remains blocked on ledger-zeta development and the Riemann hypothesis (M-001). The structure is referenced by forty downstream sites including PathSpace.interp for admissible path combinations, CostAlgebra.reciprocal_preserves_cost and reciprocal_comp_reciprocal for J-automorphisms, GaugeVsParams.alphaInv_dimensionless and curvature_gauge_invariant, and CrystalSymmetry.essentialSymmetry. It touches the open question of a first-principles RS derivation of γ via harmonic ledger structure or zeta zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.