alpha_inv_CODATA
plain-language theorem explainer
This definition supplies the CODATA 2022 central value for the inverse fine-structure constant as a real number. Physicists comparing Recognition Science predictions to experiment cite it when anchoring the alpha band. The declaration is a direct numerical assignment tagged with simp for automatic reduction in downstream calculations.
Claim. $alpha^{-1} := 137.035999177$ (CODATA 2022 central value).
background
The module quarantines all external empirical calibration data so the pure cost-first derivation from the Recognition Composition Law stays independent of measurement. This definition supplies the measured inverse fine-structure constant solely for comparison with RS-native constants. No upstream lemmas are required; the value enters as an external anchor.
proof idea
Direct numerical assignment of the real number 137.035999177 with the simp attribute attached.
why it matters
It populates the EmpiricalAnchors structure and supports the positivity lemma alpha_inv_CODATA_pos. In the Recognition framework this anchors the alpha band (137.030 to 137.039) against experiment while preserving separation between derived constants and measured values. The module policy ensures the RCL core never imports external data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.