withinSigma
plain-language theorem explainer
withinSigma defines the predicate that a predicted real value lies within n standard deviations of an empirical measurement. Researchers anchoring Recognition Science constants to CODATA data cite it to quantify agreement with experiment. The definition is a direct encoding of the absolute-difference interval as a Prop.
Claim. The proposition $|predicted - empirical| ≤ n · σ$ holds for given real numbers predicted, empirical, σ and n.
background
The ExternalAnchors module is the single quarantined location for CODATA 2022 empirical calibration data. Core Recognition Science derivations in Cost and Constants proceed from the Recognition Composition Law without importing external values. This predicate supplies a reusable statistical test for comparing a derived constant to a measured anchor.
proof idea
One-line definition that directly translates the standard n-sigma interval into the Prop |predicted - empirical| ≤ n * sigma.
why it matters
It is the immediate parent of within3Sigma, which hard-codes the conventional 3-sigma threshold for external validation. The definition supports mechanical separation between pure cost-first derivations and empirical checks, enabling direct comparison of quantities such as alpha to the CODATA band without contaminating the RCL core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.