pith. machine review for the scientific record. sign in
structure definition def or abbrev moderate

or

show as:
view Lean formalization →

The Euler-Mascheroni constant γ is defined as the limit of the nth harmonic number minus ln n. Recognition Science researchers working on number-theoretic constants would cite this when linking zeta functions to physical parameters. The declaration is a direct definition that imports the standard limit expression from Mathlib with no proof obligations.

claimThe Euler-Mascheroni constant is defined by $γ := lim_{n→∞} (H_n - ln n) ≈ 0.57721$, where $H_n = ∑_{k=1}^n 1/k$ is the nth harmonic number.

background

The module formalizes C-011 for the Euler-Mascheroni constant in the Recognition Science framework. Constants are bundled via the structure Constants from LawOfExistence, which packages Knet, Cproj, Ceng, Cdisp with the nonnegativity condition on Knet. The zeta function is the arithmetic function that equals 1 on all positive integers. Upstream results include the from theorem that extracts four structural conditions from seven axioms, the and theorem supplying an explicit log-derivative bound M on the disk, and the constant scalar field definition.

proof idea

This is a definition that directly references the standard limit expression for the Euler-Mascheroni constant from Mathlib. No lemmas or tactics are invoked beyond the open Real namespace.

why it matters in Recognition Science

The definition feeds into forty downstream sites, including PathSpace.interp for admissible path interpolation, CostAlgebra results on reciprocal maps preserving J-cost, Bridge.GaugeVsParams theorems establishing that α^{-1} is dimensionless, and Chemistry.CrystalSymmetry counts of Bravais lattices. It addresses the C-011 registry item on γ's role, with the open question of a first-principles RS derivation remaining blocked on ledger-zeta development and the Riemann hypothesis (M-001).

formal statement (Lean)

  16structure or zeta zeros; not yet developed.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Constants
  21namespace EulerMascheroni
  22
  23open Real
  24
  25/-! ## Definition and Bounds (from Mathlib) -/
  26
  27/-- γ = Euler-Mascheroni constant = lim_{n→∞} (H_n - ln n) ≈ 0.5772. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.