eV_to_J

formal source

  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)
  79
  80/-- Adjacent rungs scale by φ. -/
  81theorem phi_energy_rung_step (n : ℝ) :
  82    phi_energy_rung (n + 1) = phi_energy_rung n * phi := by
  83  unfold phi_energy_rung
  84  rw [Real.rpow_add phi_pos, Real.rpow_one]