Constants Euler Mascheroni Euler Mascheroni Bounds

The proved bounds

The Euler-Mascheroni constant, usually written γ, is the number that measures how much the harmonic series 1 + 1/2 + 1/3 + ... drifts away from the natural logarithm. Its defining formula is γ = lim (H_n − ln n), where H_n is the sum of the first n reciprocals, and its value is about 0.5772. It appears throughout number theory and physics: in the average number of divisors of an integer, in the Mertens theorems on prime distribution, and in renormalization calculations in quantum field theory. A famous open question is whether γ is irrational; no one has proved it is, and no one has proved it is rational.

What is proved is a narrow numerical window. The constant is greater than 1/2 and less than 2/3. That fact is not new, but it now lives in a machine-checked library of formal theorems, where every step of the proof is verified by a computer. The library proves the stronger pair 1/2 < γ < 2/3 and also the looser bound 0 < γ < 1, along with the immediate consequences that γ is positive and not equal to zero. These are exact formal statements, not numerical approximations with error bars.

In Recognition Science, the framework models physical constants as forced by a discrete record of events it calls a ledger. The Euler-Mascheroni constant is registered as item C-011, and its role is a target, not a result. The framework's own derivation of γ from first principles remains open, blocked on the Riemann hypothesis and on a ledger-zeta connection that has not been developed. The proved bounds are a formal foundation, not an explanation of where γ comes from.

The framework does make a structural prediction about a future derivation: if it succeeds, γ will be expressed as a closed-form function of the golden ratio φ and zeta values ζ(2), ζ(3), and so on. The named falsifier is a discovery that γ is algebraically independent of φ and all ζ(n). That prediction is a hypothesis, not a theorem, and the bounds in this section do not depend on it.

/-- Numerical bounds: 1/2 < γ < 2/3. -/
theorem gamma_numerical_bounds : (1/2 : ℝ) < gamma ∧ gamma < 2/3 :=
  ⟨Real.one_half_lt_eulerMascheroniConstant, Real.eulerMascheroniConstant_lt_two_thirds⟩

/-- **C-011 Status**: γ is well-defined; RS derivation OPEN.

    γ appears in:
    - Renormalization (QFT)
    - Prime counting (Mertens)
    - Riemann zeta ζ(s)

    Full derivation from RS: BLOCKED on M-001 (Riemann hypothesis)
    and development of ledger–zeta connection. -/
theorem euler_mascheroni_bounds : 0 < gamma ∧ gamma < 1 :=
  ⟨gamma_pos, lt_of_lt_of_le gamma_lt_two_thirds (by norm_num)⟩

/-- **OPEN target**: γ is irrational.

    Status: not proved in general mathematics (or here).
    RS perspective: γ's appearance in physics suggests it derives from
    the same φ-ladder structure as other constants. The irrationality
    would follow from the unique solvability of the ledger harmonic
    equations. -/
def target_gamma_irrational : Prop := Irrational gamma

What this page does not claim

This section does not claim that Recognition Science derives the value of γ from first principles. This section does not claim that γ is irrational, which remains open in general mathematics. This section does not claim the structural prediction is a theorem; it is a hypothesis with a named falsifier.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/EulerMascheroni.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: