IndisputableMonolith.Constants.EulerMascheroni
This module adds the Euler-Mascheroni constant γ to the Recognition Science constants collection. It records the classical limit definition together with positivity, numerical bounds, and an irrationality conjecture. Workers who embed standard mathematical constants into RS-native units cite these entries for consistency checks. The module is purely definitional with supporting lemmas.
claim$γ = lim_{n→∞} (H_n - ln n) ≈ 0.5772$
background
The upstream Constants module supplies the RS time quantum τ₀ = 1 tick. This module extends that collection by importing the Euler-Mascheroni constant, defined exactly as the limit of the difference between the nth harmonic number and the natural logarithm. In the RS setting, constants are carried in native units tied to the forcing chain and the phi-ladder; γ enters through its appearance in harmonic asymptotics and logarithmic integrals.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies γ for the broader Constants framework. It records the standard definition and basic properties that later results may invoke when comparing RS-derived constants (such as those fixed by T5 J-uniqueness or T6 phi) against classical mathematical constants.
scope and limits
- Does not derive γ from the forcing chain or Recognition Composition Law.
- Does not express γ in terms of phi or other RS-native quantities.
- Does not prove irrationality of γ; only states a conjecture.
- Does not link γ to spatial dimension D=3 or the eight-tick octave.
depends on (1)
declarations in this module (12)
-
structure
or -
abbrev
gamma -
theorem
gamma_pos -
theorem
gamma_lt_two_thirds -
theorem
gamma_numerical_bounds -
theorem
euler_mascheroni_bounds -
theorem
euler_mascheroni_implies_pos -
theorem
euler_mascheroni_implies_ne_zero -
theorem
gamma_irrational_conjecture -
theorem
gamma_bounds_optimal -
theorem
gamma_rs_prediction -
theorem
gamma_gap_analysis