hartreeRydbergScoreCardCert_holds
plain-language theorem explainer
The declaration certifies existence of a record confirming that the dimensionless Hartree energy over electron rest mass equals 1 over alphaInv squared, the Rydberg ratio equals half that value, and the Bohr radius over reduced Compton wavelength equals alphaInv, all within the stated numerical intervals. A physicist checking precision constant derivations or Recognition Science alpha scaling would cite this result to anchor the P1-C02 through P1-C04 rows. The proof is a term-mode construction that directly assembles the closed equalities and a
Claim. There exists a certificate such that the Hartree energy ratio to electron rest energy equals $1/alphaInv^2$, the Rydberg ratio equals $1/(2 alphaInv^2)$, the Bohr radius over reduced Compton wavelength equals $alphaInv$, and each ratio lies inside its certified numerical interval: Hartree in (5.32e-5, 5.33e-5), Rydberg in (2.66e-5, 2.665e-5), and Bohr in (137.030, 137.039).
background
The module certifies dimensionless ratios for Hartree energy (P1-C04), Rydberg constant (P1-C02), and Bohr radius (P1-C03) using the RS inverse fine-structure constant alphaInv. The structure HartreeRydbergScoreCardCert packages three closed equalities together with three interval brackets. Upstream, row_hartree_over_rest_eq states row_hartree_over_rest = 1 / alphaInv ^ 2 by field_simp after unfolding alpha, while row_hartree_over_rest_bracket supplies the numerical bounds via lower and upper lemmas. Parallel equalities and brackets hold for the Rydberg and Bohr rows, with the Bohr equality being reflexivity and its bracket obtained from alphaInv_gt and alphaInv_lt.
proof idea
The proof is a term-mode construction of the HartreeRydbergScoreCardCert record. It supplies the three closed equalities directly from row_hartree_over_rest_eq, row_rydberg_over_rest_eq and row_bohr_over_reduced_compton_eq, then inserts the three bracket theorems row_hartree_over_rest_bracket, row_rydberg_over_rest_bracket and row_bohr_over_reduced_compton_bracket.
why it matters
This theorem certifies the unit-free scorecard for the three constants that the Recognition Science alpha derivation must reproduce. It draws on the Constants interface from CPM.LawOfExistence and closes the numerical check against the alpha band (137.030, 137.039). The result supports the claim that alpha^2 scaling emerges from the J-uniqueness and phi-ladder steps without additional hypotheses. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.