schwinger_in_range
plain-language theorem explainer
Recognition Science derives the leading Schwinger correction to the electron g-factor as a small positive quantity below 0.002. Experimental physicists validating the phi-ladder model against g-minus-2 data would reference this bound. The proof combines the positivity of the term with an upper estimate obtained by inserting the RS value of the inverse fine-structure constant and using pi greater than 3.
Claim. $0 < 1/ (r_s^{-1} · 2π) < 0.002$, where $r_s^{-1}$ denotes the Recognition Science value of the inverse fine-structure constant near 137.036.
background
The module develops the electron anomalous magnetic moment within the Recognition Science φ-ladder framework, as described in the paper RS_Electron_g_minus_2.tex. The Schwinger term is defined locally as 1 divided by the product of the RS inverse fine-structure constant and twice π, matching the standard leading QED correction α/(2π) expressed in RS-native units. Upstream results supply the positivity of this ratio of positive reals and the upper bound obtained by rewriting the inequality and invoking π > 3 to reach 0.548144π > 1.
proof idea
The proof is a one-line term-mode wrapper that constructs the conjunction by directly applying the positivity theorem for the Schwinger term together with the theorem establishing its strict upper bound of 0.002.
why it matters
This bound supplies the numerical interval required by the downstream electron g-factor theorem, which shows the g-factor exceeds the Dirac value of 2. It anchors the leading term in the RS calculation of the anomalous magnetic moment, consistent with the eight-tick octave and the alpha inverse band (137.030, 137.039). The result closes the verification step for the Schwinger contribution without touching open questions on higher-order terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.