E_PBM_pos
plain-language theorem explainer
The lemma establishes that the photobiomodulation energy E_PBM is strictly positive. Researchers modeling RS-coherent light therapy cite it when proving wavelength positivity or energy bounds for the rung-6 photon. The proof is a direct one-line application of the multiplication-positivity lemma to the factors phi and the eV-to-joules conversion.
Claim. $0 < E_{PBM}$ where $E_{PBM} := phi · eV_to_J$ is the photobiomodulation energy in joules.
background
The module formalizes Recognition Science foundations for a photobiomodulation device operating on the phi-energy ladder. E_PBM is defined as the rung-6 energy phi · eV_to_J, corresponding to the coherence quantum scaled to approximately 1.618 eV. The upstream lemma eV_to_J_pos establishes positivity of the conversion factor by direct norm_num evaluation on the constant definition.
proof idea
The proof is a one-line wrapper that applies the mul_pos lemma to phi_pos and eV_to_J_pos.
why it matters
This positivity lemma feeds directly into div_bounds_of_E_PBM (which transfers bounds to arbitrary positive numerators) and lambda_PBM_pos (which derives wavelength positivity via division). It anchors the therapeutic wavelength calculation at rung 6 of the phi-ladder, placing the device output inside the red/near-IR window while respecting the eight-tick octave neutrality constraint of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.