row_rydberg_over_rest_bracket
plain-language theorem explainer
The theorem certifies that the dimensionless Rydberg-to-electron-rest-energy ratio lies strictly between 2.66e-5 and 2.665e-5. Researchers checking Recognition Science predictions for the fine-structure constant against CODATA data would cite this interval. The proof is a one-line term that pairs the separately proved lower and upper bounds.
Claim. Let $r = E_R / (m_e c^2)$ denote the dimensionless Rydberg-to-rest-energy ratio, where $E_R$ is the Rydberg energy. Then $2.66 times 10^{-5} < r < 2.665 times 10^{-5}$.
background
The module records unit-free ratios for atomic constants using the certified RS inverse fine-structure constant alphaInv. The Rydberg ratio is defined as alpha squared over 2 and corresponds to the P1-C02 entry in the physical derivation plan, sitting beside the Hartree energy ratio (alpha squared) and Bohr radius ratio (one over alpha).
proof idea
The proof is a one-line term wrapper that constructs the conjunction from row_rydberg_over_rest_lower and row_rydberg_over_rest_upper.
why it matters
This bracket completes the interval for the Rydberg ratio and feeds directly into hartreeRydbergScoreCardCert_holds, which assembles the full scorecard certificate. It fills the P1-C02 step of the derivation plan and confirms consistency with the alpha band (137.030, 137.039) from the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.