IndisputableMonolith.Constants.Codata

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Constants
   5
   6/-!
   7# CODATA / SI Reference Constants (Quarantined)
   8
   9This module contains **empirical** (SI/CODATA) numeric constants:
  10
  11- `c` (speed of light)
  12- `hbar` (reduced Planck constant)
  13- `G` (Newton's gravitational constant)
  14
  15These are intentionally **quarantined from the certified surface**. The top-level
  16certificate chain (and its import-closure) should not depend on these numeric values.
  17
  18If you need these constants for numeric comparisons or empirical reports, import this
  19module explicitly.
  20-/
  21
  22noncomputable section
  23
  24/-! ## CODATA 2018 reference values -/
  25
  26/-- Speed of light (exact SI definition). -/
  27@[simp] noncomputable def c : ℝ := 299792458
  28
  29/-- Reduced Planck constant (CODATA 2018). -/
  30@[simp] noncomputable def hbar : ℝ := 1.054571817e-34
  31
  32/-- Gravitational constant (CODATA 2018). -/
  33@[simp] noncomputable def G : ℝ := 6.67430e-11
  34
  35lemma c_pos : 0 < c := by unfold c; norm_num
  36lemma hbar_pos : 0 < hbar := by unfold hbar; norm_num
  37lemma G_pos : 0 < G := by unfold G; norm_num
  38
  39lemma c_ne_zero : c ≠ 0 := ne_of_gt c_pos
  40lemma hbar_ne_zero : hbar ≠ 0 := ne_of_gt hbar_pos
  41lemma G_ne_zero : G ≠ 0 := ne_of_gt G_pos
  42
  43end
  44
  45end Constants
  46end IndisputableMonolith
  47