planck_h

formal source

  45/-! ## CODATA Physical Constants (SI, for wavelength calculation) -/
  46
  47/-- Planck constant (J·s), CODATA 2024 -/
  48def planck_h : ℝ := 6.62607015e-34
  49
  50/-- Speed of light (m/s), exact -/
  51def speed_of_light : ℝ := 299792458
  52
  53/-- Electron volt to joules conversion, exact -/
  54def eV_to_J : ℝ := 1.602176634e-19
  55
  56lemma planck_h_pos : 0 < planck_h := by norm_num [planck_h]
  57lemma speed_of_light_pos : 0 < speed_of_light := by norm_num [speed_of_light]
  58lemma eV_to_J_pos : 0 < eV_to_J := by norm_num [eV_to_J]
  59
  60/-! ## Section 1: The φ-Energy Ladder
  61
  62The φ-energy ladder maps integer rungs to photon energies.
  63E_base = φ⁻⁵ eV is the recognition coherence quantum.
  64Each rung scales by one power of φ. -/
  65
  66/-- Base energy of the φ-ladder: E_base = φ⁻⁵ eV (recognition coherence quantum).
  67    In joules: φ⁻⁵ × 1.602e-19. -/
  68noncomputable def E_base : ℝ := phi ^ (-(5 : ℝ)) * eV_to_J
  69
  70lemma E_base_pos : 0 < E_base :=
  71  mul_pos (Real.rpow_pos_of_pos phi_pos _) eV_to_J_pos
  72
  73/-- The φ-energy ladder: E(n) = E_base · φⁿ.
  74    Maps real-valued rung n to photon energy in joules. -/
  75noncomputable def phi_energy_rung (n : ℝ) : ℝ := E_base * phi ^ n
  76
  77lemma phi_energy_rung_pos (n : ℝ) : 0 < phi_energy_rung n :=
  78  mul_pos E_base_pos (Real.rpow_pos_of_pos phi_pos n)