within3Sigma
within3Sigma encodes the standard 3-sigma agreement test between a predicted constant and its empirical counterpart. Researchers validating Recognition Science outputs against CODATA data cite this predicate. It reduces directly to the general withinSigma definition by fixing the multiplier at 3.
claimThe predicate holds when $|p - e| ≤ 3σ$, where $p$ is the predicted value, $e$ the empirical anchor, and $σ$ its reported uncertainty.
background
ExternalAnchors isolates all CODATA and empirical calibration data from the core Recognition Science derivations. The module policy requires that the cost-first core never imports it, preserving the purity of the RCL-based derivations. All entries carry the external_anchor attribute for audit.
proof idea
One-line wrapper that applies withinSigma with the constant multiplier 3.
why it matters in Recognition Science
This definition supplies the conventional 3-sigma criterion used to anchor Recognition Science constants to experimental data. It implements the external calibration policy stated in the module documentation, allowing comparison to CODATA 2022 values while keeping empirical inputs quarantined. No parent theorems depend on it yet, but it supports validation of derived constants such as alpha and G.
scope and limits
- Does not perform hypothesis testing or compute p-values.
- Does not adjust for correlations between multiple anchors.
- Does not handle asymmetric or non-Gaussian uncertainties.
formal statement (Lean)
231def within3Sigma (predicted empirical sigma : ℝ) : Prop :=
proof body
Definition body.
232 withinSigma predicted empirical sigma 3
233
234/-! ## Positivity and Basic Facts -/
235