CODATA_alpha_inv
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value from the Recognition Science functional equation.
- Does not encode the experimental uncertainty interval.
- Does not connect the constant to the phi-ladder mass formula or the eight-tick octave.
Lean usage
example (w8 : ℝ) : ℝ := additive_residual w8formal statement (Lean)
167def CODATA_alpha_inv : ℝ := 137.035999206
proof body
Definition body.
168
169/-- The precision hypothesis: the full series converges to CODATA. -/