row_rydberg_over_rest
plain-language theorem explainer
row_rydberg_over_rest supplies the P1-C02 dimensionless ratio of Rydberg energy to electron rest energy as alpha squared over two. Researchers verifying the Hartree-Rydberg scorecard against CODATA data cite this entry when confirming the alpha-squared scaling in Recognition Science units. The definition is realized as a direct one-line algebraic expression that unfolds from the imported alpha constant.
Claim. The dimensionless ratio of Rydberg energy to electron rest energy equals $E_R / (m_e c^2) = alpha^2 / 2$, where $alpha$ denotes the fine-structure constant.
background
The HartreeRydbergScoreCard module records three unit-free ratios drawn from the physical derivation plan: Hartree energy over rest energy equals alpha squared, Rydberg over rest energy equals alpha squared over two, and Bohr radius over reduced Compton wavelength equals alpha inverse. These ratios use the certified inverse fine-structure constant alphaInv to produce interval bounds that target CODATA measurements. The alpha definition imported from the Alpha module supplies the base value as one over alphaInv.
proof idea
This is a one-line definition that directly assigns the expression alpha squared divided by two, relying on the alpha definition from the Alpha module.
why it matters
The definition supplies the rydberg_closed field inside the HartreeRydbergScoreCardCert structure and feeds the equality and bracket theorems that certify the P1-C02 row. It anchors the scorecard's match to the alpha band (137.030, 137.039) and the dimensionless scaling required by the Recognition Science forcing chain. The entry closes one of the three Phase-1 constant rows without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.