row_electron_ae_leading_upper
plain-language theorem explainer
The upper bound on the leading Schwinger term for the electron anomalous magnetic moment is established as strictly less than 0.001162. Researchers validating Recognition Science constants against QED precision data would cite this when checking the alpha-derived prediction. The tactic proof rewrites the term to the reciprocal of twice pi times alpha inverse, chains strict inequalities on pi and alphaInv through multiplication lemmas, then closes with linarith.
Claim. Let $a_e^{(1)} = 1/(2 pi alpha_inv)$ denote the leading Schwinger term, where $alpha_inv$ is the Recognition Science inverse fine-structure constant. Then $a_e^{(1)} < 0.001162$.
background
The ElectronGMinus2ScoreCard module isolates Phase 1 row P1-C05, the leading Schwinger term $a_e^{(1)} = alpha/(2 pi)$. The definition row_electron_ae_leading computes this term directly from the fine-structure constant. Upstream, alphaInv is the dimensionless inverse fine-structure constant given by alpha_seed times exp of minus f_gap over alpha_seed, and alphaInv_gt supplies the concrete lower bound 137.030 < alphaInv. The module documentation states that this slice lies within 0.3 percent of the CODATA value, while the full g-2 row remains partial until higher loops are derived from RS primitives.
proof idea
The proof first rewrites the leading term to 1 over 2 pi alphaInv using the equality lemma. It invokes div_lt_iff0 with the positivity theorem ae_den_pos to convert the goal into 1 < 0.001162 times 2 pi alphaInv. Separate have blocks establish 2 times 3.1415 < 2 pi via Real.pi_gt_d6, then 2 pi times 137.030 < 2 pi alphaInv via alphaInv_gt, followed by multiplication of the inequality by the positive constant 0.001162. The final linarith closes the chain.
why it matters
This supplies the upper half of the bracket theorem row_electron_ae_leading_bracket, which asserts 0.001161 < leading term < 0.001162. The module documentation positions the result as the theorem-grade slice for the Schwinger term and notes its 0.3 percent proximity to CODATA. The bound draws on the alphaInv construction from the structural seed and gap, consistent with the Recognition Science forcing chain that fixes constants without adjustable parameters. The open question remains derivation of the higher-order QED loop corrections from RS primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.