pith. machine review for the scientific record. sign in
theorem proved term proof

phi_energy_rung_zero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  88theorem phi_energy_rung_zero : phi_energy_rung 0 = E_base := by

proof body

Term-mode proof.

  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. -/

depends on (5)

Lean names referenced from this declaration's body.