IndisputableMonolith.Constants.EulerMascheroni
This module defines the Euler-Mascheroni constant γ as the limit of H_n minus ln n inside the Recognition Science constants library. It supplies positivity results, numerical bounds, and an RS-specific prediction for γ. Researchers matching the phi-ladder to observed constants cite these definitions for calibration. The module consists of definitions and supporting lemmas with no central proof.
claim$γ := lim_{n→∞} (H_n - ln n) ≈ 0.5772$
background
The module resides in the Constants domain of Recognition Science and imports the parent IndisputableMonolith.Constants where the fundamental time quantum is fixed as τ₀ = 1 tick. It introduces γ together with sibling objects that encode positivity, bounds, and an RS prediction. These objects operate in RS-native units and support numerical checks against the phi-ladder.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module supplies γ for the Recognition Science constant derivations. It feeds the parent Constants module by providing bounds and the gamma_rs_prediction that align with the phi-ladder and alpha band. The definitions close a numerical interface between standard constants and the T5 J-uniqueness and T6 phi fixed-point steps.
scope and limits
- Does not derive γ from the Recognition Composition Law.
- Does not prove the gamma_irrational_conjecture.
- Does not link γ to the eight-tick octave or spatial dimension D=3.
- Does not embed γ into the mass formula yardstick.
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