analysis
plain-language theorem explainer
Canonical summary record of the fine-structure inverse gap: RS underpredicts CODATA by ~0.001 (8 ppm), the size matches a next-order curvature scale, no single counting-layer formula hits exactly, and three resolution paths stay open. Cited wherever the status of the α⁻¹ correction is needed. Constructed as the default inhabitant of the correction-analysis structure.
Claim. The current $\alpha^{-1}$ correction analysis is the default summary record: the required shift is positive ($\sim 0.001$, about 8 ppm), its magnitude is natural for a next-order geometric term, candidate counting-layer expressions only bracket the target ($0.000994$ to $0.001214$), and three resolution paths remain open.
background
The module studies the residual between the Recognition Science fine-structure prediction 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 needed additive correction is $\delta_2 \approx +0.00110$. Admissible corrections must be built from counting-layer integers and the transcendentals $\pi,\varphi$, stay $\sim 10^{-3}$, introduce no free parameters, and admit a cube-geometry reading.
CorrectionAnalysis is a pure summary structure whose fields are fixed strings: sign (RS underpredicts), magnitude scale ($\sim 10^{-3}$), the observation that no single candidate is exact, and a short list of remaining resolution paths (exact higher-order cube term, refined weight, or external-anchor adjustment).
proof idea
One-line default structure instance. Every field of the summary structure already carries a default string (or list of strings), so := {} fills the record with those defaults and nothing else is proved.
why it matters
Pins the official status of the $\alpha^{-1}$ gap inside the verification layer: positive 8 ppm residual, natural next-order size, candidates only bracket, three open paths. That status is the reference point for the module's candidate bounds and for any downstream consumer that needs a single named handle on the correction analysis (chemistry ionic-bond proxies, nuclear $\varphi$-tiers, dimensioned constants, gap-weight formulae). In the broader framework it sits next to the RS $\alpha^{-1}$ band $(137.030, 137.039)$ and records that the seed formula alone does not yet close CODATA; the open geometric-term path is the live research question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.