IndisputableMonolith.Constants.ExternalAnchors

   1import Mathlib
   2
   3/-!
   4# External Anchors: CODATA and Empirical Calibration Data
   5
   6## PURPOSE
   7
   8This module is the **single quarantined location** for all empirical calibration data
   9that enters Recognition Science from external sources. The cost-first core of RS
  10derives everything from the RCL primitive—this module exists solely to enable
  11comparison with experimental reality.
  12
  13## POLICY
  14
  15**The cost-first core MUST NOT import this module.**
  16
  17Any module that imports `ExternalAnchors` is explicitly acknowledging that it
  18uses external calibration data. This creates a clean mechanical separation:
  19
  20- `IndisputableMonolith.Cost` → pure cost derivation (no external data)
  21- `IndisputableMonolith.Constants` → RS-native units only
  22- `IndisputableMonolith.Constants.ExternalAnchors` → CODATA/empirical values
  23
  24## MECHANICAL LABELING
  25
  26All definitions in this module are tagged with `@[external_anchor]` for audit purposes.
  27Tools can grep for this attribute to identify calibration seams.
  28
  29## VERSION
  30
  31CODATA 2022 values (SI 2019 redefinition).
  32
  33-/
  34
  35namespace IndisputableMonolith
  36namespace Constants
  37namespace ExternalAnchors
  38
  39/-! ### Mechanical Labeling Convention
  40
  41All definitions in this module follow a naming convention for audit purposes:
  42- Suffix `_SI` for SI-unit values
  43- Suffix `_CODATA` for CODATA central values
  44- Suffix `_uncertainty` for measurement uncertainties
  45
  46Additionally, use the doc tag `**EXTERNAL ANCHOR**` in all docstrings.
  47Tools can grep for this pattern to identify calibration seams:
  48  `grep -r "EXTERNAL ANCHOR" IndisputableMonolith/`
  49-/
  50
  51/-- **EXTERNAL ANCHOR** marker type for documentation.
  52    This doesn't affect code but signals calibration dependence. -/
  53abbrev ExternalAnchorMarker := Unit
  54
  55/-! ## CODATA 2022 Fundamental Constants
  56
  57**EXTERNAL ANCHOR SECTION**
  58
  59These are the official CODATA 2022 values. The SI 2019 redefinition makes
  60several of these exact by definition.
  61-/
  62
  63section CODATAFundamental
  64
  65/-- **EXTERNAL ANCHOR**: Speed of light in vacuum (exact, SI 2019 definition).
  66    c = 299792458 m/s -/
  67@[simp]
  68noncomputable def c_SI : ℝ := 299792458
  69
  70/-- **EXTERNAL ANCHOR**: Reduced Planck constant (exact, SI 2019 definition).
  71    ℏ = 1.054571817... × 10⁻³⁴ J·s -/
  72@[simp]
  73noncomputable def hbar_SI : ℝ := 1.054571817e-34
  74
  75/-- **EXTERNAL ANCHOR**: Planck constant (exact, SI 2019 definition).
  76    h = 6.62607015 × 10⁻³⁴ J·s -/
  77@[simp]
  78noncomputable def h_SI : ℝ := 6.62607015e-34
  79
  80/-- **EXTERNAL ANCHOR**: Elementary charge (exact, SI 2019 definition).
  81    e = 1.602176634 × 10⁻¹⁹ C -/
  82@[simp]
  83noncomputable def e_SI : ℝ := 1.602176634e-19
  84
  85/-- **EXTERNAL ANCHOR**: Boltzmann constant (exact, SI 2019 definition).
  86    k_B = 1.380649 × 10⁻²³ J/K -/
  87@[simp]
  88noncomputable def kB_SI : ℝ := 1.380649e-23
  89
  90/-- **EXTERNAL ANCHOR**: Avogadro constant (exact, SI 2019 definition).
  91    N_A = 6.02214076 × 10²³ mol⁻¹ -/
  92@[simp]
  93noncomputable def NA_SI : ℝ := 6.02214076e23
  94
  95/-- **EXTERNAL ANCHOR**: Gravitational constant (CODATA 2022, measured).
  96    G = 6.67430(15) × 10⁻¹¹ m³/(kg·s²)
  97    Relative uncertainty: 2.2 × 10⁻⁵ -/
  98@[simp]
  99noncomputable def G_SI : ℝ := 6.67430e-11
 100
 101/-- **EXTERNAL ANCHOR**: Gravitational constant uncertainty (1σ). -/
 102noncomputable def G_SI_uncertainty : ℝ := 0.00015e-11
 103
 104end CODATAFundamental
 105
 106/-! ## Fine Structure Constant
 107
 108**EXTERNAL ANCHOR SECTION**
 109
 110The electromagnetic coupling constant, dimensionless.
 111-/
 112
 113section FineStructure
 114
 115/-- **EXTERNAL ANCHOR**: Fine structure constant (CODATA 2022).
 116    α = 7.2973525643(11) × 10⁻³
 117    Relative uncertainty: 1.5 × 10⁻¹⁰ -/
 118@[simp]
 119noncomputable def alpha_CODATA : ℝ := 7.2973525643e-3
 120
 121/-- **EXTERNAL ANCHOR**: Fine structure constant uncertainty (1σ). -/
 122noncomputable def alpha_CODATA_uncertainty : ℝ := 0.0000000011e-3
 123
 124/-- **EXTERNAL ANCHOR**: Inverse fine structure constant (CODATA 2022).
 125    α⁻¹ = 137.035999177(21) -/
 126@[simp]
 127noncomputable def alpha_inv_CODATA : ℝ := 137.035999177
 128
 129/-- **EXTERNAL ANCHOR**: α⁻¹ uncertainty (1σ). -/
 130noncomputable def alpha_inv_CODATA_uncertainty : ℝ := 0.000000021
 131
 132/-- **EXTERNAL ANCHOR**: α⁻¹ empirical bounds (±3σ). -/
 133structure AlphaInvBounds where
 134  lower : ℝ := 137.035999114  -- -3σ
 135  upper : ℝ := 137.035999240  -- +3σ
 136  codata_year : Nat := 2022
 137
 138/-- **EXTERNAL ANCHOR** -/
 139def alpha_inv_bounds : AlphaInvBounds := {}
 140
 141end FineStructure
 142
 143/-! ## Particle Masses
 144
 145**EXTERNAL ANCHOR SECTION**
 146
 147Dimensionless mass ratios (from PDG 2024 / CODATA 2022).
 148-/
 149
 150section MassRatios
 151
 152/-- **EXTERNAL ANCHOR**: Electron mass (CODATA 2022).
 153    m_e = 9.1093837139(28) × 10⁻³¹ kg
 154    m_e = 0.51099895069(16) MeV/c² -/
 155@[simp]
 156noncomputable def electron_mass_kg : ℝ := 9.1093837139e-31
 157
 158/-- **EXTERNAL ANCHOR** -/
 159@[simp]
 160noncomputable def electron_mass_MeV : ℝ := 0.51099895069
 161
 162/-- **EXTERNAL ANCHOR**: Muon mass (PDG 2024).
 163    m_μ = 105.6583755(23) MeV/c² -/
 164@[simp]
 165noncomputable def muon_mass_MeV : ℝ := 105.6583755
 166
 167/-- **EXTERNAL ANCHOR**: Proton mass (CODATA 2022).
 168    m_p = 938.27208943(29) MeV/c² -/
 169@[simp]
 170noncomputable def proton_mass_MeV : ℝ := 938.27208943
 171
 172/-- **EXTERNAL ANCHOR**: Electron-to-muon mass ratio (CODATA 2022).
 173    m_e / m_μ = 4.83633169(11) × 10⁻³ -/
 174@[simp]
 175noncomputable def electron_muon_ratio_CODATA : ℝ := 4.83633169e-3
 176
 177/-- **EXTERNAL ANCHOR** -/
 178noncomputable def electron_muon_ratio_uncertainty : ℝ := 0.00000011e-3
 179
 180/-- **EXTERNAL ANCHOR**: Proton-to-electron mass ratio (CODATA 2022).
 181    m_p / m_e = 1836.15267343(11) -/
 182@[simp]
 183noncomputable def proton_electron_ratio_CODATA : ℝ := 1836.15267343
 184
 185/-- **EXTERNAL ANCHOR** -/
 186noncomputable def proton_electron_ratio_uncertainty : ℝ := 0.00000011
 187
 188/-- **EXTERNAL ANCHOR**: Mass ratio bounds (±3σ for comparison). -/
 189structure MassRatioBounds where
 190  electron_muon_lower : ℝ := 4.83633136e-3
 191  electron_muon_upper : ℝ := 4.83633202e-3
 192  proton_electron_lower : ℝ := 1836.15267310
 193  proton_electron_upper : ℝ := 1836.15267376
 194  codata_year : Nat := 2022
 195
 196/-- **EXTERNAL ANCHOR** -/
 197def mass_ratio_bounds : MassRatioBounds := {}
 198
 199end MassRatios
 200
 201/-! ## Calibration Seam Interface
 202
 203**EXTERNAL ANCHOR SECTION**
 204
 205These structures provide a clean interface for modules that need to compare
 206RS predictions to empirical values.
 207-/
 208
 209/-- **EXTERNAL ANCHOR**: A complete set of external anchors for comparison. -/
 210structure EmpiricalAnchors where
 211  /-- α⁻¹ central value -/
 212  alpha_inv : ℝ := alpha_inv_CODATA
 213  alpha_inv_sigma : ℝ := alpha_inv_CODATA_uncertainty
 214  /-- Electron-muon ratio -/
 215  electron_muon : ℝ := electron_muon_ratio_CODATA
 216  electron_muon_sigma : ℝ := electron_muon_ratio_uncertainty
 217  /-- Proton-electron ratio -/
 218  proton_electron : ℝ := proton_electron_ratio_CODATA
 219  proton_electron_sigma : ℝ := proton_electron_ratio_uncertainty
 220  /-- Source year -/
 221  codata_year : Nat := 2022
 222
 223/-- **EXTERNAL ANCHOR**: The default empirical anchors (CODATA 2022). -/
 224noncomputable def empiricalAnchors : EmpiricalAnchors := {}
 225
 226/-- **EXTERNAL ANCHOR**: Check if a predicted value is within nσ of the empirical anchor. -/
 227def withinSigma (predicted empirical sigma : ℝ) (n : ℝ) : Prop :=
 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
 262