within3Sigma
plain-language theorem explainer
The within3Sigma definition supplies the standard 3σ comparison predicate for predicted versus measured constants. Calibration routines comparing Recognition Science outputs to CODATA anchors cite it directly. The definition is a direct one-line specialization of the general withinSigma predicate at n=3.
Claim. $|predicted - empirical| ≤ 3σ$ for real numbers predicted, empirical and uncertainty σ.
background
The ExternalAnchors module is the single quarantined location for all empirical calibration data entering Recognition Science. Its policy requires that any import signals use of external data, keeping the RCL core and RS-native units isolated from measured constants. The upstream withinSigma predicate is defined by |predicted - empirical| ≤ n * sigma for supplied n.
proof idea
One-line wrapper that applies withinSigma with the constant argument 3.
why it matters
This definition supplies the conventional 3σ threshold used when anchoring Recognition Science predictions to external data. It sits in the ExternalAnchors module whose purpose is to enable comparison with experiment while preserving separation from the cost-first core. No downstream theorems depend on it yet; it serves as a reusable predicate for future calibration statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.