required_correction
plain-language theorem explainer
Defines the exact additive gap δ₂ between the CODATA inverse fine-structure constant and the RS-native α⁻¹. Anyone checking candidate cube-geometry corrections or the 8 ppm α closure cites this scalar. It is a one-line difference of two named reals, not a derived identity.
Claim. The required correction is the real number $\delta_2 := \alpha^{-1}_{\mathrm{CODATA}} - \alpha^{-1}_{\mathrm{RS}}$, where $\alpha^{-1}_{\mathrm{CODATA}} = 137.035999177$ is the external CODATA 2022 anchor and $\alpha^{-1}_{\mathrm{RS}}$ is the canonical RS exponential-resummation expression (seed times $\exp(-f_{\mathrm{gap}}/\mathrm{seed})$).
background
This module studies the residual needed to close the gap between the Recognition Science inverse fine-structure constant and the CODATA value. The RS construction gives $\alpha^{-1}_{\mathrm{RS}} \approx 137.0349$ via the seed $4\pi\cdot 11$ and an exponential gap factor; CODATA sits at $137.035999177(21)$. The module frames an admissible correction $\delta_2 \approx +0.00110$ that must be built from counting-layer integers and $\pi,\varphi$ only, stay $\sim 10^{-3}$, introduce no free parameters, and admit a cube-geometry reading.
Upstream, alphaInv is the dimensionless RS inverse-α (canonical exponential resummation, nothing fit to CODATA). The exact infrared target $\alpha^{-1}(0)=137.035999$ remains an open boundary condition. alpha_inv_CODATA is the external 2022 anchor used only for comparison, not as an internal free parameter.
proof idea
Pure definition: subtract the RS-native inverse fine-structure constant from the CODATA anchor. No lemmas, no tactics; the body is the difference of two @[simp] reals. Downstream positivity and window theorems unfold this name and apply linarith to interval facts about the two summands.
why it matters
This scalar is the yardstick against which every candidate cube-geometry correction is scored in the same module. Parent results correction_positive and correction_positive_of_alphaInv_lt turn a strict inequality $\alpha^{-1}{\mathrm{RS}} < \alpha^{-1}{\mathrm{CODATA}}$ into $0 < \delta_2$; correction_window_from_current_bounds pins $\delta_2$ inside $(-0.004, 0.006)$ from present interval arithmetic.
In the broader RS picture the α band sits near $(137.030, 137.039)$; closing the residual 8 ppm without new parameters is the remaining honesty gap on the electromagnetic sector. The definition itself does not choose a candidate; it only names the target that candidates 1–4 are measured against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.