within3Sigma

formal source

 228  |predicted - empirical| ≤ n * sigma
 229
 230/-- **EXTERNAL ANCHOR**: Standard comparison: within 3σ. -/
 231def within3Sigma (predicted empirical sigma : ℝ) : Prop :=
 232  withinSigma predicted empirical sigma 3
 233
 234/-! ## Positivity and Basic Facts -/
 235
 236lemma c_SI_pos : 0 < c_SI := by norm_num [c_SI]
 237lemma hbar_SI_pos : 0 < hbar_SI := by norm_num [hbar_SI]
 238lemma G_SI_pos : 0 < G_SI := by norm_num [G_SI]
 239lemma alpha_inv_CODATA_pos : 0 < alpha_inv_CODATA := by norm_num [alpha_inv_CODATA]
 240lemma electron_mass_MeV_pos : 0 < electron_mass_MeV := by norm_num [electron_mass_MeV]
 241lemma muon_mass_MeV_pos : 0 < muon_mass_MeV := by norm_num [muon_mass_MeV]
 242lemma proton_mass_MeV_pos : 0 < proton_mass_MeV := by norm_num [proton_mass_MeV]
 243
 244/-! ## Module Summary
 245
 246This module provides:
 2471. **CODATA 2022 fundamental constants** (c, ℏ, h, e, k_B, N_A, G)
 2482. **Fine structure constant** (α, α⁻¹ with uncertainties)
 2493. **Particle mass ratios** (m_e/m_μ, m_p/m_e with uncertainties)
 2504. **Comparison utilities** (bounds checking, σ-based comparison)
 251
 252**Import Policy**: Only import this module when you need to compare RS predictions
 253to empirical values. The cost-first core should never import this module.
 254
 255**Mechanical Audit**: All definitions are tagged with `@[external_anchor]`.
 256Run `grep -r "external_anchor" IndisputableMonolith/` to find all calibration seams.
 257-/
 258
 259end ExternalAnchors
 260end Constants
 261end IndisputableMonolith