alphaInv_pos
plain-language theorem explainer
The positivity of the RS-derived inverse fine-structure constant is established here. Researchers bounding the leading Schwinger contribution to the electron anomaly would invoke this result to justify divisions by alphaInv in the scorecard rows. The proof reduces immediately to the certified lower bound via linear arithmetic.
Claim. $0 < alphaInv$ where $alphaInv$ is the dimensionless inverse fine-structure constant obtained from the structural seed and gap via exponential resummation.
background
This module certifies bounds on the leading Schwinger term $a_e^{(1)} = alpha / (2 pi)$ of the electron g-2 anomaly, using the RS interval for $alphaInv$. The constant is defined as $alphaInv := alpha_seed * exp(-f_gap / alpha_seed)$, with $alpha_seed$ and $f_gap$ drawn from the eight-tick structure in the Recognition framework. The upstream theorem alphaInv_gt supplies the concrete lower bound $137.030 < alphaInv$, itself obtained from log_phi_gt_0481 and W8 bounds.
proof idea
This is a one-line wrapper that applies the linarith tactic to the hypothesis alphaInv_gt.
why it matters
This positivity lemma is invoked repeatedly in the Hartree-Rydberg scorecard to discharge the non-zero denominators in expressions such as row_hartree_over_rest = 1 / alphaInv^2. It supports the electron g-2 module's leading-term bounds and closes the positivity requirement for the alpha band (137.030, 137.039) in the Recognition framework. The parent theorems include the various row_...eq and row..._lower/upper statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.