codataAlphaInverse
plain-language theorem explainer
The declaration supplies the CODATA 2022 numerical value of the inverse fine-structure constant as a real number. Researchers verifying the Recognition Science alpha band would cite this constant when confirming that the experimental datum falls inside the predicted interval. It is introduced as a direct numerical assignment with no further computation or derivation.
Claim. The CODATA 2022 value of the inverse fine-structure constant is given by $137.035999084$.
background
The module records an explicit numerical check in the provenance chain that begins with the J-functional equation J(x) = (x + x^{-1})/2 - 1, proceeds through the forced self-similar fixed point phi, and reaches D = 3 spatial dimensions via the eight-tick octave. This structure determines 44 recognition frequency slots and produces the RS formula alpha^{-1} = 44 pi exp(-8 ln(phi)/(44 pi)). The present definition simply stores the experimental CODATA 2022 datum for direct comparison against the derived band (137.030, 137.039).
proof idea
The definition is a direct numerical assignment of the real number 137.035999084.
why it matters
This definition supplies the experimental anchor inside the AlphaProvenanceCert structure, which certifies that the CODATA value lies inside the RS-predicted interval. It completes the explicit chain from the J-uniqueness theorem through phi and D = 3 to the alpha formula, confirming numerical agreement with observation. The module states that the entire provenance is a structural theorem with zero axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.