EmpiricalAnchors
plain-language theorem explainer
This structure collects CODATA 2022 values for the inverse fine-structure constant, electron-muon mass ratio, and proton-electron mass ratio along with their 1σ uncertainties. Researchers comparing Recognition Science predictions to laboratory data would cite it to measure numerical agreement. The definition simply assembles the pre-existing sibling constants into a single record with no further computation.
Claim. A record containing the central value and 1σ uncertainty of the inverse fine-structure constant, the electron-to-muon mass ratio and its uncertainty, the proton-to-electron mass ratio and its uncertainty, and the CODATA release year 2022.
background
The module quarantines all external calibration data so that the cost-first core of Recognition Science, which derives everything from the Recognition Composition Law, never imports measured numbers. EmpiricalAnchors therefore serves only as an audit seam for later comparison steps. Its fields are initialized from the sibling definitions alpha_inv_CODATA (137.035999177), alpha_inv_CODATA_uncertainty (2.1e-8), electron_muon_ratio_CODATA (4.83633169e-3), and the corresponding proton-electron quantities, all tagged with the external_anchor attribute.
proof idea
The declaration is a structure definition whose fields receive default values directly from the sibling CODATA constants defined earlier in the same module. No lemmas, tactics, or reductions are applied; the body is a plain record literal.
why it matters
It supplies the concrete numbers consumed by the downstream definition empiricalAnchors, which instantiates the default record for use in comparison lemmas. The structure therefore closes the mechanical separation required by the module policy: core derivations remain free of external data while still permitting quantitative checks against the alpha band (137.030, 137.039) and other RS-native constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.