row_hartree_over_rest_upper
plain-language theorem explainer
The theorem proves the dimensionless Hartree-to-rest-energy ratio lies strictly below 5.33e-5. Precision-constant workers in Recognition Science cite it to close the upper edge of the alpha interval. The proof rewrites the definition via the equality lemma, clears the positive denominator, and finishes with nlinarith on the certified bounds 137.030 < alphaInv < 137.039.
Claim. The dimensionless ratio of Hartree energy to electron rest energy satisfies $E_H/(m_e c^2) < 5.33×10^{-5}$.
background
The module supplies unit-free ratios for the Hartree energy (P1-C04), Rydberg scale, and Bohr radius using the RS inverse fine-structure constant. row_hartree_over_rest is defined as alpha squared, where alpha equals 1/alphaInv and alphaInv is the canonical exponential resummation alpha_seed * exp(-(f_gap/alpha_seed)). Upstream lemmas establish positivity of alphaInv, the equality row_hartree_over_rest = 1/alphaInv^2, and the interval bounds alphaInv_gt and alphaInv_lt.
proof idea
The tactic proof rewrites via row_hartree_over_rest_eq, obtains positivity of alphaInv squared from alphaInv_pos, clears the denominator with div_lt_iff, proves 137.030 squared is less than alphaInv squared by nlinarith on alphaInv_gt and alphaInv_lt, checks the numerical inequality 1 < 5.33e-5 * 137.030 squared by norm_num, and closes with nlinarith.
why it matters
It supplies the upper half of the bracket theorem row_hartree_over_rest_bracket that records the tight interval for the Hartree ratio. The result fills the P1-C04 slot in the physical derivation plan by confirming that the RS-derived alpha squared sits inside the measured window. It thereby validates the alpha scaling forced by J-uniqueness and the eight-tick octave in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.