HartreeRydbergScoreCardCert
plain-language theorem explainer
The HartreeRydbergScoreCardCert structure packages the exact algebraic relations and numerical interval bounds for three dimensionless ratios derived from the RS inverse fine-structure constant. Researchers working on precision constants or RS derivations would cite it to confirm the Hartree energy over electron rest energy equals one over alpha inverse squared, the Rydberg ratio is half that, and the Bohr radius over reduced Compton wavelength equals alpha inverse, all within tight brackets matching CODATA ranges. The definition assembles the六
Claim. Let $a = 1/alphaInv$ denote the RS inverse fine-structure constant. The certificate requires the dimensionless Hartree-to-rest-energy ratio to satisfy $E_H/(m_e c^2) = 1/a^2$, the Rydberg-to-rest-energy ratio to satisfy $E_R/(m_e c^2) = 1/(2 a^2)$, the Bohr-to-reduced-Compton ratio to satisfy $a_0/λbar_C = a$, together with the interval constraints $5.32×10^{-5} < E_H/(m_e c^2) < 5.33×10^{-5}$, $2.66×10^{-5} < E_R/(m_e c^2) < 2.665×10^{-5}$, and $137.030 < a < 137.039$.
background
This module records the unit-free content of three Phase-1 rows from the physical derivation plan: the Hartree energy ratio (P1-C04), Rydberg constant ratio (P1-C02), and Bohr radius ratio (P1-C03). The inverse fine-structure constant alphaInv is defined in the Alpha module as the product of a structural seed and an exponential factor involving the gap function, producing the value near 137.036 with no free parameters. The row definitions set the Hartree ratio to alpha squared, the Rydberg ratio to alpha squared over 2, and the Bohr ratio directly to alphaInv, where alpha is the reciprocal of alphaInv.
proof idea
As a structure definition this declaration simply introduces a record type whose six fields are the three closed-form equalities and three bracket inequalities. No lemmas or tactics are invoked inside the declaration; the equalities are later witnessed by row_hartree_over_rest_eq and its companions, while the numerical brackets are supplied by the corresponding bracket lemmas in the same module.
why it matters
This structure serves as the bundled certificate that the RS alphaInv reproduces the known dimensionless relations for the Hartree energy, Rydberg energy, and Bohr radius to high precision. It is instantiated by the theorem hartreeRydbergScoreCardCert_holds, which populates the fields using the equality and bracket lemmas. In the Recognition framework it closes the Phase-1 constant scorecard for these three quantities, confirming that the structural alpha inverse lies in the target band (137.030, 137.039) and that the derived ratios match the expected alpha squared and alpha squared over 2 scalings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.