IndisputableMonolith.Constants.HartreeRydbergScoreCard
The HartreeRydbergScoreCard module supplies interval definitions and bracket lemmas for the dimensionless Hartree/rest-energy and Rydberg/rest-energy ratios under the P1-C04 label. Researchers verifying Recognition Science constants against the phi-ladder mass formula would cite these rows when checking consistency with the supplied alpha interval. The module structure consists of direct applications of the imported alpha bounds via interval arithmetic, with no internal proofs.
claimThe module defines the interval for the Hartree-to-rest-energy ratio and the Rydberg-to-rest-energy ratio, both derived from the bound $137.030 < alpha^{-1} < 137.039$ supplied by the AlphaBounds module.
background
Recognition Science works in native units with $c=1$, $hbar=phi^{-5}$, and $alpha^{-1}$ required to lie inside the interval (137.030, 137.039). The upstream Alpha module defines the inverse fine-structure constant while the AlphaBounds module supplies the rigorous symbolic interval bounds on that quantity. The present module then assembles the P1-C04 scorecard by constructing rows that convert those alpha bounds into dimensionless energy ratios.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the concrete numerical content for the P1-C04 step that sits inside the constants domain of the forcing chain. It feeds any later verification that the yardstick times phi to a power reproduces observed Hartree and Rydberg values. No downstream uses are recorded in the current graph.
scope and limits
- Does not derive the alpha interval bounds.
- Does not compute absolute energies or masses.
- Does not incorporate QED corrections beyond the leading alpha dependence.
- Does not address the full eight-tick octave structure.
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