CODATA_alpha_inv
plain-language theorem explainer
The definition supplies the 2022 CODATA numerical target for the inverse fine-structure constant. Researchers comparing Recognition Science series expansions for alpha to experiment cite it to quantify the residual that higher-order voxel-seam corrections must close. It is introduced as a direct real-number constant with no internal derivation or proof steps.
Claim. The 2022 CODATA value of the inverse fine-structure constant is defined by the real number $137.035999206$.
background
Recognition Science obtains the fine-structure constant from three ingredients: the geometric seed $4π×11≈138.230$, the gap weight $w_8·lnφ≈1.198$, and the first curvature correction $δ_1=-103/(102π^5)≈-0.00330$. These produce an additive approximation near 137.035 and an exponential approximation near 137.037; the module adopts the experimental CODATA value as the explicit convergence target for the infinite series of higher-order corrections $∑δ_n$ on the cube Q3. The local setting is the formalization of combinatorial sums over face-wallpaper pairs weighted by the $Z_2^5$ half-period measure, with the series required to be alternating and convergent.
proof idea
This declaration is a direct definition of the real constant. No lemmas or tactics are applied; the value is simply bound to the literal 137.035999206.
why it matters
The constant anchors the AlphaPrecisionHypothesis structure, which demands that the partial sums of the delta series converge to it, and appears inside the definitions of additive_residual and exponential_residual that measure the remaining gap. It realizes the Recognition Science alpha band (137.030,137.039) as the limit point of the T5 J-uniqueness and T6 phi fixed-point steps. The open deliverable it highlights is the explicit computation of δ2 and higher terms on Q3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.