E_PBM_pos
plain-language theorem explainer
The lemma proves that the photobiomodulation energy E_PBM is strictly positive. Modelers of RS-coherent light therapy devices cite it when establishing wavelength positivity or transferring bounds to numerators. The proof is a one-line application of the mul_pos lemma to the positivity of phi and the eV-to-J conversion factor.
Claim. $0 < E_{PBM}$ where $E_{PBM} = phi * eV_to_J$ and $eV_to_J$ denotes the electronvolt-to-joule conversion factor.
background
The module develops RS foundations for photobiomodulation devices on the phi-energy ladder, with $E(n) = E_base * phi^n$ and $E_base = phi^{-5}$ eV. E_PBM is the noncomputable definition $phi * eV_to_J$, realizing the rung-6 energy in joules. The upstream result eV_to_J_pos states $0 < eV_to_J$ by direct norm_num evaluation of the conversion constant.
proof idea
One-line wrapper that applies the mul_pos lemma to phi_pos and eV_to_J_pos.
why it matters
Feeds the division-bounds helper div_bounds_of_E_PBM and the wavelength-positivity lemma lambda_PBM_pos. It supplies the basic positivity needed for the rung-6 therapeutic wavelength in the phi-ladder, consistent with the eight-tick octave and recognition coherence quantum. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.