CorrectionAnalysis
plain-language theorem explainer
Bundles the present status of the ~0.001 gap between RS and CODATA inverse fine-structure values: RS underpredicts by about 8 ppm, the scale matches a next-order curvature term, no single counting-layer candidate hits exactly, and three resolution paths remain open. Anyone tracking the alpha derivation cites this as the living summary object. It is a plain structure of string fields with defaults, not a proved theorem.
Claim. A record summarizing the $\alpha^{-1}$ correction analysis: (i) the needed shift is positive (RS underpredicts CODATA by $\sim 0.001$, about 8 ppm); (ii) its magnitude is $\sim 10^{-3}$, consistent with a next-order curvature term; (iii) no single counting-layer expression matches exactly (candidates bracket $\delta_2$ in $[0.000994, 0.001214]$); (iv) three resolution paths remain: exact higher-order cube geometry, scale-dependent RS evaluation of $\alpha$, or a QED vacuum-polarization bridge from the RS scale to the CODATA extraction point.
background
The module studies the residual between the Recognition Science inverse fine-structure constant and CODATA. With $\alpha^{-1}{\mathrm{RS}} = 4\pi\cdot 11 - w_8\ln\varphi + 103/(102\pi^5) \approx 137.0349$ and $\alpha^{-1}{\mathrm{CODATA}} = 137.035999206(21)$, the required additive correction is $\delta_2 \approx +0.00110$.
Admissible corrections must be built from counting-layer integers and the fixed transcendentals $\pi,\varphi$; stay $\sim 10^{-3}$ relative to the $O(10^2)$ seed; introduce no free parameters; and admit a combinatorial reading inside the cube geometry (the eight-tick / $D=3$ setting of the forcing chain).
Sibling lemmas in the module compute the required correction from interval bounds on $\alpha^{-1}$ and evaluate several candidate expressions. This structure does not recompute those numbers; it packages the qualitative conclusions of that evaluation.
proof idea
No proof. The declaration is a structure whose four fields are string (or list-of-string) defaults encoding the current narrative: positive sign, natural $10^{-3}$ magnitude, absence of an exact single-term match among the candidates, and the three open resolution paths. Instantiation is by empty braces, which inherits those defaults.
why it matters
Closes the documentation layer of the alpha-correction program: after numerical candidates are checked against $\delta_2$, this object is the single place that records sign, scale, mismatch, and remaining paths. Downstream, analysis is the canonical empty instance used as the module's summary value.
In the broader framework it sits under the alpha band target $\alpha^{-1}\in(137.030,137.039)$ and the constants fixed by the forcing chain ($\varphi$ from T6, eight-tick octave from T7). Paths A–C name the open work: a geometric higher-order term from cube topology, a recognition-scale (not $Q^2=0$) reading of RS alpha, or an explicit QED VP bridge. Until one path is discharged, the 8 ppm gap remains a characterized residual rather than a closed identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.