empiricalAnchors
plain-language theorem explainer
The definition supplies the default record of external calibration values drawn from CODATA 2022, including the inverse fine-structure constant with its uncertainty and selected particle mass ratios. Researchers comparing Recognition Science predictions against experiment reference this record to obtain the empirical targets. The implementation is a direct instantiation of the EmpiricalAnchors structure using its field defaults.
Claim. The default instance of the structure containing the central value and uncertainty for $α^{-1}$, the electron-muon mass ratio, and the proton-electron mass ratio, each taken from CODATA 2022, is denoted by the record whose fields are initialized to those tabulated values.
background
This module isolates all external empirical data so that the pure cost-first derivations remain independent of measurement. The structure EmpiricalAnchors collects the central values and uncertainties for $α^{-1}$, the electron-muon mass ratio, and the proton-electron mass ratio, each initialized to the corresponding CODATA 2022 entry. Upstream structures such as those in NucleosynthesisTiers and PhiForcingDerived supply the theoretical tiers and J-cost definitions against which these anchors are compared.
proof idea
The definition is a one-line wrapper that constructs the EmpiricalAnchors record by invoking the default values declared in the structure fields.
why it matters
This definition supplies the sole entry point for CODATA calibration data into the Recognition Science framework, enabling quantitative tests of predictions such as the alpha band and mass ladder against experiment. It implements the separation policy stated in the module documentation, ensuring that the RCL-derived core remains free of external constants. No parent theorems appear in the used-by graph, indicating that direct usage sites remain to be added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.