row_rydberg_over_rest_lower
plain-language theorem explainer
The theorem proves that the dimensionless Rydberg-to-rest-energy ratio exceeds 2.66e-5 when the RS inverse fine-structure constant lies in its certified interval. Precision-constant derivations and Recognition Science scorecard checks cite this bound to anchor the P1-C02 row. The tactic proof rewrites the ratio via its explicit algebraic form in alphaInv, invokes positivity and the upper interval bound, then reduces the claim to a numerical inequality settled by linear arithmetic.
Claim. $2.66 times 10^{-5} < alpha^2 / 2$, where $alpha$ is the fine-structure constant obtained as the reciprocal of the RS-derived inverse $alpha_{rm inv} in (137.030, 137.039)$.
background
The module supplies unit-free ratios for the Hartree, Rydberg, and Bohr scales using the RS inverse fine-structure constant. The Rydberg-over-rest ratio is defined as $alpha^2 / 2$ and equals $1 / (2 alphaInv^2)$ by the equality theorem. Upstream results provide positivity of alphaInv together with the strict bounds $137.030 < alphaInv < 137.039$ from the AlphaBounds module and the algebraic identity that expresses the ratio explicitly in terms of alphaInv.
proof idea
The proof rewrites the target via row_rydberg_over_rest_eq to obtain the form $1 / (2 alphaInv^2)$. It establishes positivity of the denominator with sq_pos_of_ne_zero and nlinarith. The inequality is rearranged by lt_div_iff0, the upper bound alphaInv < 137.039 is substituted, and the resulting numerical claim is verified by norm_num followed by nlinarith.
why it matters
This lower bound completes the sandwich in the downstream bracket theorem row_rydberg_over_rest_bracket. It fills the P1-C02 entry of the physical derivation plan by showing that the RS alpha produces a Rydberg scale inside the certified interval (137.030, 137.039). The result relies on the parameter-free exponential resummation for alphaInv and supports the overall dimensionless scorecard without SI-unit bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.