row_hartree_over_rest
plain-language theorem explainer
The definition supplies the dimensionless Hartree to electron-rest-energy ratio as the square of the fine-structure constant. Atomic physicists verifying RS predictions for atomic energy scales against CODATA would cite this row when assembling the scorecard. It is introduced by a direct one-line assignment that pulls alpha from the upstream Alpha module.
Claim. $E_h/(m_e c^2)=α^2$
background
The HartreeRydbergScoreCard module records three unit-free ratios from atomic physics: Hartree energy over rest energy (P1-C04), Rydberg energy over rest energy (P1-C02), and Bohr radius over reduced Compton wavelength (P1-C03). All three are expressed using the RS-certified inverse fine-structure constant alphaInv restricted to the interval (137.030, 137.039). The upstream alpha definition supplies alpha := 1/alphaInv, so the Hartree ratio collapses to alpha squared.
proof idea
The declaration is a one-line definition that directly sets the Hartree ratio equal to alpha squared, drawing alpha from the imported Alpha module.
why it matters
It supplies the hartree_closed field inside the HartreeRydbergScoreCardCert structure that bundles the closed expressions and interval bounds for the full scorecard. The definition fills the P1-C04 slot in the physical derivation plan and sits downstream of the alpha definition while feeding the bracket theorems that place the ratio inside (5.32e-5, 5.33e-5).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.