row_rydberg_over_rest_eq
plain-language theorem explainer
The equality establishes that the dimensionless ratio of Rydberg energy to electron rest energy equals the reciprocal of twice the square of the inverse fine-structure constant. Physicists verifying Recognition Science predictions for hydrogen atom scales would cite this when confirming consistency with the derived fine-structure value. The proof is a direct algebraic unfolding of the ratio definition followed by field simplification using positivity of the inverse constant.
Claim. The dimensionless Rydberg energy ratio satisfies $E_R / (m_e c^2) = 1 / (2 (α^{-1})^2)$, where $α^{-1}$ is the inverse fine-structure constant derived from the structural seed and gap.
background
The HartreeRydbergScoreCard module records dimensionless ratios for atomic scales using the Recognition Science inverse fine-structure constant. The Rydberg ratio is defined as the square of the fine-structure constant divided by two, with the fine-structure constant itself the reciprocal of the inverse constant. This setup captures the unit-free content of the Rydberg constant relative to the electron rest energy, listed as P1-C02 in the physical derivation plan.
proof idea
The proof is a term-mode reduction. It unfolds the definitions of the Rydberg ratio and the fine-structure constant, then applies field_simp to clear the denominator using the positivity theorem for the inverse constant.
why it matters
This equality supplies the closed symbolic form for the Rydberg row and is invoked inside the certification theorem for the full Hartree-Rydberg-Bohr score card. It implements the P1-C02 entry from the physical derivation plan. In the Recognition framework it connects the derived inverse fine-structure constant to the observed Rydberg scale, consistent with the alpha band interval (137.030, 137.039). It touches no open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.