IndisputableMonolith.Constants.HartreeRydbergScoreCard
The HartreeRydbergScoreCard module assembles definitions and interval statements for the dimensionless Hartree to rest-energy ratio labeled P1-C04 together with related Rydberg ratios. Researchers checking consistency of derived constants against fine-structure bounds would cite it. The module organizes its content as rows of equalities and bounds drawn from the imported Alpha and AlphaBounds modules.
claimThe principal objects are the ratios $r_H = E_{ m Hartree}/(m_e c^2)$ and $r_R = E_{ m Rydberg}/(m_e c^2)$ together with their lower and upper bounds obtained from the interval on $\\,\alpha^{-1}$.
background
The module belongs to the Constants domain of Recognition Science and imports Alpha for fine-structure definitions plus AlphaBounds for interval arithmetic on $\alpha^{-1}$. The upstream AlphaBounds module states that it supplies rigorous bounds on alphaInv using the symbolic derivation. The local setting places all constants in RS-native units with $c=1$ and derives them from the J-cost function and phi-ladder.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module contributes the P1-C04 entry to the constants scorecard and supports verification steps that rely on the alpha interval. It supplies the Hartree and Rydberg rows that sit downstream of the alpha bounds and upstream of any global constant-consistency checks in the framework.
scope and limits
- Does not derive the ratios from the J-function or phi-ladder.
- Does not address G, hbar, or mass-ladder formulas.
- Does not perform experimental comparisons.
- Does not extend the alpha interval beyond the imported bounds.
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