row_bohr_over_reduced_compton_bracket
plain-language theorem explainer
This theorem proves the dimensionless Bohr radius to reduced Compton wavelength ratio lies strictly between 137.030 and 137.039. Researchers compiling Recognition Science constant scorecards or checking fine-structure predictions would cite it for the P1-C03 row. The proof is a one-line term that pairs the lower and upper bounds already established for alphaInv.
Claim. $137.030 < a_0 / {bar lambda}_C < 137.039$, where $a_0 / {bar lambda}_C := alpha^{-1}$ and $alpha^{-1}$ denotes the certified inverse fine-structure constant from the Recognition Science derivation.
background
The module records unit-free ratios for the Hartree energy, Rydberg constant, and Bohr radius expressed through the inverse fine-structure constant. The sibling definition row_bohr_over_reduced_compton sets this ratio exactly to alphaInv. Upstream theorems alphaInv_gt and alphaInv_lt supply the concrete interval bounds on alphaInv that arise from the gap term and seed construction in the alpha bounds module.
proof idea
The proof is a one-line term wrapper that constructs the conjunction by directly supplying the pair alphaInv_gt and alphaInv_lt.
why it matters
It supplies the bracketed interval for the Bohr row inside hartreeRydbergScoreCardCert_holds, completing the P1-C03 entry of the physical derivation plan. The result confirms that the RS-derived alpha^{-1} sits inside the target interval (137.030, 137.039) required by the framework landmark for the fine-structure constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.