E_base_pos

formal source

  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]
  85  ring
  86
  87/-- Rung 0 recovers E_base. -/
  88theorem phi_energy_rung_zero : phi_energy_rung 0 = E_base := by
  89  simp [phi_energy_rung]
  90
  91/-! ## Section 2: Therapeutic Wavelength (Rung 6 → 766 nm)
  92
  93Rung 6 on the φ-energy ladder gives E = φ eV, because
  94E(6) = E_base · φ⁶ = φ⁻⁵ · φ⁶ eV = φ eV.
  95The corresponding wavelength λ = hc/(φ eV) ≈ 766 nm falls
  96squarely in the red/near-IR photobiomodulation window. -/
  97
  98/-- Photobiomodulation energy: E_PBM = φ eV. -/
  99noncomputable def E_PBM : ℝ := phi * eV_to_J
 100