row_rydberg_over_rest_upper
plain-language theorem explainer
The dimensionless Rydberg-to-rest-energy ratio is bounded above by 2.665 times 10 to the minus 5. A physicist verifying Recognition Science predictions for atomic energy scales against the certified alpha interval would cite this bound. The tactic proof rewrites the ratio to one over two alphaInv squared then closes via nlinarith on the interval bounds and a numerical check.
Claim. Let $E_R$ denote the Rydberg energy and $m_e c^2$ the electron rest energy. The dimensionless ratio satisfies $E_R / (m_e c^2) < 2.665 × 10^{-5}$, where the inverse fine-structure constant lies in $(137.030, 137.039)$.
background
Recognition Science records unit-free ratios for atomic constants in the HartreeRydbergScoreCard module. The Rydberg-to-rest ratio is defined as alpha squared over 2 and equals one over two times alphaInv squared, with alphaInv the structural inverse fine-structure constant alpha_seed times exp of minus f_gap over alpha_seed. The module imports Alpha and AlphaBounds to certify the ratios inside the alpha band (137.030, 137.039).
proof idea
The proof rewrites the target via row_rydberg_over_rest_eq to obtain one over two alphaInv squared. Positivity of two alphaInv squared follows from sq_pos_of_ne_zero applied to alphaInv_pos then nlinarith. The inequality is rewritten with div_lt_iff₀. nlinarith on alphaInv_gt and alphaInv_lt yields alphaInv squared greater than 137.030 squared. norm_num confirms one less than 2.665e-5 times two times 137.030 squared, after which nlinarith finishes.
why it matters
Together with the matching lower bound this feeds row_rydberg_over_rest_bracket, which pins the ratio inside (2.66e-5, 2.665e-5). It completes the P1-C02 entry in the scorecard from the physical derivation plan. The bound rests on the Recognition Science alphaInv derivation and the alpha band, consistent with the forcing chain from the structural seed through the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.