correction_positive
plain-language theorem explainer
If the RS inverse fine-structure constant lies strictly below the CODATA anchor, the residual needed to match CODATA is positive. Anyone auditing the sign of the α-gap correction cites this. The proof unfolds the residual definition and finishes by linear arithmetic on the difference.
Claim. Let $\alpha^{-1}_{\mathrm{RS}}$ be the Recognition-Science inverse fine-structure constant and $\alpha^{-1}_{\mathrm{CODATA}}$ the CODATA 2022 anchor. Define the required correction by $\delta_2 := \alpha^{-1}_{\mathrm{CODATA}} - \alpha^{-1}_{\mathrm{RS}}$. If $\alpha^{-1}_{\mathrm{RS}} < \alpha^{-1}_{\mathrm{CODATA}}$, then $0 < \delta_2$.
background
The module studies the ~0.001 correction that closes the ~8 ppm gap between the RS construction of $\alpha^{-1}$ and the CODATA value. Numerically, $\alpha^{-1}{\mathrm{RS}} \approx 137.0349$ while $\alpha^{-1}{\mathrm{CODATA}} = 137.035999177$, so the residual is about $+0.00110$.
The RS value alphaInv is the assembled dimensionless expression (seed times an exponential gap factor; equivalently a $44\pi,\mathrm{e}^{-\cdots}$ form in the PRC presentation). It is not fit to CODATA. The CODATA figure is an external anchor. The local definition required_correction is exactly their difference: $\alpha^{-1}{\mathrm{CODATA}} - \alpha^{-1}{\mathrm{RS}}$.
Admissible corrections must be built from counting-layer integers and $(\pi,\varphi)$, stay $\sim 10^{-3}$, introduce no free parameters, and admit a cube-geometry reading. This lemma only settles the sign of the residual under the inequality hypothesis.
proof idea
Term-mode proof in two steps. Unfold required_correction to the difference $\alpha^{-1}{\mathrm{CODATA}} - \alpha^{-1}{\mathrm{RS}}$. The hypothesis is precisely that this difference is positive, so linarith closes $0 < \delta_2$. No external lemmas beyond the definition and linear arithmetic.
why it matters
Fixes the sign of the residual that the rest of AlphaCorrectionAnalysis must explain: any candidate $\delta_2$ from cube geometry is measured against a positive target of order $10^{-3}$. The module evaluates several combinatorial candidates against that window; this theorem is the sign gate for that comparison.
In the broader RS picture it sits inside the $\alpha^{-1}$ band near $(137.030, 137.039)$: the construction lands slightly low of CODATA, so the correction is an additive positive shift, not a subtraction. Downstream use is currently empty in the graph; the immediate consumers are the sibling window and candidate lemmas in the same module. It does not close the OPEN infrared boundary-condition status of $\alpha^{-1}(0)$ noted on alphaInv.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.