c_SI

formal source

  38/-! ## SI definitional constants (not fit parameters) -/
  39
  40/-- SI-definitional speed of light in meters per second (exact). -/
  41def c_SI : ℝ := 299792458
  42
  43lemma c_SI_pos : 0 < c_SI := by
  44  norm_num [c_SI]
  45
  46/-- SI-definitional Planck constant \(h\) (exact, 2019 SI): 6.62607015×10⁻³⁴ J·s.
  47
  48We write this exactly as a rational: 662607015 / 10^42. -/
  49noncomputable def h_SI : ℝ :=
  50  (662607015 : ℝ) / ((10 : ℝ) ^ (42 : ℕ))
  51
  52lemma h_SI_pos : 0 < h_SI := by
  53  unfold h_SI
  54  have hnum : (0 : ℝ) < (662607015 : ℝ) := by norm_num
  55  have hden : (0 : ℝ) < (10 : ℝ) ^ (42 : ℕ) := by
  56    exact pow_pos (by norm_num : (0 : ℝ) < 10) 42
  57  exact div_pos hnum hden
  58
  59/-- Reduced Planck constant \(\hbar = h/(2\pi)\) (exact given SI definition of \(h\)). -/
  60noncomputable def hbar_SI : ℝ :=
  61  h_SI / (2 * Real.pi)
  62
  63lemma hbar_SI_pos : 0 < hbar_SI := by
  64  unfold hbar_SI
  65  have hden : (0 : ℝ) < 2 * Real.pi := by
  66    have h2 : (0 : ℝ) < 2 := by norm_num
  67    exact mul_pos h2 Real.pi_pos
  68  exact div_pos h_SI_pos hden
  69
  70/-! ## Calibration protocol (measurement framework) -/
  71