E_base_pos
plain-language theorem explainer
The lemma proves positivity of the base energy E_base on the phi-ladder, where E_base equals phi to the power minus five times the eV-to-joule conversion. Photobiomodulation device modelers cite it to ensure every rung energy remains positive before scaling by phi to the power n. The proof is a one-line wrapper applying the multiplication-positivity rule to the positivity of phi raised to a real power and the conversion constant.
Claim. $0 < E_ {base}$ where $E_{base} := phi^{-5} · eV_{to J}$ and $eV_{to J}$ denotes the conversion factor from electronvolts to joules.
background
The Photobiomodulation Device module formalizes the phi-energy ladder E(n) = E_base · phi^n for RS-coherent light therapy. The module doc defines E_base as the recognition coherence quantum phi^{-5} eV, converted to joules by multiplication with the eV-to-J factor. This setting targets rung 6 yielding phi eV at approximately 766 nm in the red/near-IR therapeutic window, with the 8-beat modulation pattern satisfying neutrality.
proof idea
The proof is a one-line wrapper that applies mul_pos to Real.rpow_pos_of_pos phi_pos _ and the upstream lemma eV_to_J_pos.
why it matters
This lemma supplies the base positivity needed for the downstream result phi_energy_rung_pos, which states 0 < phi_energy_rung n by multiplying E_base_pos with Real.rpow_pos_of_pos phi_pos n. It anchors the phi-ladder construction in the photobiomodulation framework, consistent with the eight-tick octave and the forcing chain landmarks T5 through T8. The module references RS_Biophase_Light_Device_Spec for device specification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.