row_hartree_over_rest_bracket
plain-language theorem explainer
The theorem proves that the dimensionless Hartree energy to electron rest-energy ratio lies strictly between 5.32e-5 and 5.33e-5. Researchers validating the RS-derived fine-structure constant against CODATA data would cite this interval bound. The proof is a one-line term that pairs the separately established lower and upper bound theorems.
Claim. $5.32 10^{-5} < E_h / (m_e c^2) < 5.33 10^{-5}$
background
The HartreeRydbergScoreCard module records dimensionless ratios for phase-1 constants using the certified RS inverse fine-structure constant alphaInv in (137.030, 137.039). row_hartree_over_rest is defined as alpha squared and satisfies row_hartree_over_rest = 1 / alphaInv squared by the upstream equation theorem row_hartree_over_rest_eq. The lower bound theorem row_hartree_over_rest_lower and upper bound theorem row_hartree_over_rest_upper each rewrite to this equation and apply interval inequalities on alphaInv squared.
proof idea
The proof is a one-line term that constructs the conjunction by pairing row_hartree_over_rest_lower with row_hartree_over_rest_upper.
why it matters
The bracket is referenced inside hartreeRydbergScoreCardCert_holds to certify the full score card for Hartree, Rydberg, and Bohr ratios. It closes the interval requirement for P1-C04 in the physical derivation plan and aligns with the alpha band of Recognition Science. The module documentation states that an alphaInv value outside (137.030, 137.039) would falsify the claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.