phi_energy_rung_zero

formal source

  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
 101lemma E_PBM_pos : 0 < E_PBM :=
 102  mul_pos phi_pos eV_to_J_pos
 103
 104/-- E_PBM bounded by φ bounds: E_PBM ∈ (1.61, 1.62) eV. -/
 105lemma E_PBM_bounds :
 106    1.61 * eV_to_J < E_PBM ∧ E_PBM < 1.62 * eV_to_J :=
 107  ⟨mul_lt_mul_of_pos_right phi_gt_onePointSixOne eV_to_J_pos,
 108   mul_lt_mul_of_pos_right phi_lt_onePointSixTwo eV_to_J_pos⟩
 109
 110/-- E_PBM equals rung 6 on the φ-energy ladder:
 111    E_base · φ⁶ = φ⁻⁵ eV · φ⁶ = φ eV = E_PBM. -/
 112theorem E_PBM_is_rung_6 : E_PBM = phi_energy_rung 6 := by
 113  unfold E_PBM phi_energy_rung E_base
 114  have key : phi ^ (-(5 : ℝ)) * phi ^ (6 : ℝ) = phi := by
 115    rw [← Real.rpow_add phi_pos,
 116        (by norm_num : (-(5 : ℝ) + (6 : ℝ) : ℝ) = (1 : ℝ)),
 117        Real.rpow_one]
 118  have h : phi ^ (-(5 : ℝ)) * eV_to_J * phi ^ (6 : ℝ) = phi * eV_to_J := by