alphaInv_pos
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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of alphaInv beyond the supplied interval bounds.
- Does not address higher-order QED corrections to the electron anomaly.
- Does not derive the RS primitives alpha_seed or f_gap.
- Does not prove uniqueness of the alphaInv definition.
formal statement (Lean)
51private theorem alphaInv_pos : 0 < alphaInv := by
proof body
One-line wrapper that applies linarith.
52 linarith [alphaInv_gt]
53