alphaInv_pos
plain-language theorem explainer
The theorem establishes strict positivity of the RS-derived inverse fine-structure constant alphaInv. Atomic physicists computing dimensionless Hartree and Rydberg energy ratios relative to electron rest mass would cite it to justify field simplifications and denominator clearing. The proof is a one-line wrapper that feeds the lower bound alphaInv_gt into linear arithmetic.
Claim. $0 < alphaInv$ where $alphaInv := alpha_seed * exp(-f_gap / alpha_seed)$ is the dimensionless inverse fine-structure constant obtained from the structural seed and gap with no free parameters.
background
The HartreeRydbergScoreCard module records the unit-free relations $E_h / (m_e c^2) = 1/alphaInv^2$ and $E_R / (m_e c^2) = 1/(2 alphaInv^2)$ together with their certified interval bounds, using the RS inverse fine-structure constant. These correspond to the P1-C04 and P1-C02 rows of the physical derivation plan. alphaInv is defined by the canonical exponential resummation $alpha_seed * exp(-f_gap / alpha_seed)$ and is known to lie near 137.036.
proof idea
The proof is a one-line wrapper that applies the linarith tactic directly to the upstream theorem alphaInv_gt.
why it matters
This positivity result is invoked by the downstream equalities row_hartree_over_rest_eq and row_rydberg_over_rest_eq to obtain ne_of_gt alphaInv_pos for field_simp. It supplies the necessary sign information for the interval bounds on the Hartree and Rydberg ratios that target the alpha band (137.030, 137.039). The lemma therefore closes a prerequisite for the dimensionless score card in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.