row_bohr_over_reduced_compton
plain-language theorem explainer
The definition sets the dimensionless Bohr radius over reduced Compton wavelength ratio equal to the RS inverse fine-structure constant. Atomic physicists and metrologists comparing theoretical ratios to CODATA data would cite this scorecard entry. It is realized as a direct alias to the upstream alphaInv computation.
Claim. $a_0 / {}$λbar$_C = {}$α$^{-1}$ where ${}$α$^{-1}$ is the Recognition Science value of the inverse fine-structure constant.
background
The module records dimensionless ratios for Hartree energy over rest energy, Rydberg constant over rest energy, and Bohr radius over reduced Compton wavelength, all expressed via the certified RS inverse fine-structure constant. Upstream, alphaInv is defined as alpha_seed * Real.exp (-(f_gap / alpha_seed)) and supplies the numerical value near 137.036 with no free parameters. The local setting states the unit-free relations E_h / (m_e c^2) = α², E_R / (m_e c^2) = α² / 2, and a_0 / λbar_C = 1/α for direct comparison to NIST measurements.
proof idea
One-line definition that aliases the ratio directly to alphaInv.
why it matters
It supplies the bohr_closed field inside the HartreeRydbergScoreCardCert structure and supports the equality row_bohr_over_reduced_compton_eq together with the bracket theorem that confines the value inside (137.030, 137.039). The entry fills the P1-C03 row of the Phase 1 constants scorecard and anchors the alpha band inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.