IndisputableMonolith.Constants.HartreeRydbergScoreCard
This module assembles scorecard rows for the dimensionless Hartree/rest-energy ratio and Rydberg/rest-energy ratio under P1-C04. Researchers checking Recognition Science constant predictions against measured values would cite these interval definitions. The module imports alpha inverse bounds and constructs lower/upper bracket rows without internal theorems.
claimThe module defines interval rows for the Hartree/rest-energy ratio $E_H / (m_e c^2)$ and Rydberg/rest-energy ratio $E_R / (m_e c^2)$ together with their lower and upper bounds, all derived from the interval on $alphaInv$.
background
The module belongs to the Constants domain and addresses the P1-C04 dimensionless Hartree/rest-energy ratio. It imports the Alpha module for the fine-structure constant definition and the AlphaBounds module, whose doc-comment states: 'This module provides interval bounds on alphaInv using the symbolic derivation.' Recognition Science places alpha inverse inside the band (137.030, 137.039) as a consequence of the J-uniqueness and three-dimensional forcing chain.
proof idea
this is a definition module, no proofs. It defines the sibling rows row_hartree_over_rest, row_rydberg_over_rest and their lower/upper/bracket variants by direct application of the imported alpha interval bounds.
why it matters in Recognition Science
The module supplies the numerical scorecard entries for P1-C04 that close the constants verification loop. It draws directly on the alpha interval produced by the AlphaBounds module and thereby supports the alpha band required by the T5-T8 forcing chain. No downstream declarations are listed.
scope and limits
- Does not derive the alpha interval from the J-function.
- Does not compare the computed ratios to laboratory measurements.
- Does not address other constants such as G or hbar.
- Does not contain any theorem statements or sorry placeholders.
depends on (2)
declarations in this module (16)
-
def
row_hartree_over_rest -
def
row_rydberg_over_rest -
def
row_bohr_over_reduced_compton -
theorem
alphaInv_pos -
theorem
row_hartree_over_rest_eq -
theorem
row_rydberg_over_rest_eq -
theorem
row_hartree_over_rest_lower -
theorem
row_hartree_over_rest_upper -
theorem
row_hartree_over_rest_bracket -
theorem
row_rydberg_over_rest_lower -
theorem
row_rydberg_over_rest_upper -
theorem
row_rydberg_over_rest_bracket -
theorem
row_bohr_over_reduced_compton_eq -
theorem
row_bohr_over_reduced_compton_bracket -
structure
HartreeRydbergScoreCardCert -
theorem
hartreeRydbergScoreCardCert_holds