lambda_PBM_pos
plain-language theorem explainer
The lemma establishes that the photobiomodulation wavelength derived from the phi-energy ladder is strictly positive. Modelers of RS-coherent light therapy devices cite it to confirm the wavelength parameter lies in the physical domain. The proof is a direct term-mode application of positivity preservation under multiplication and division.
Claim. $0 < h c / E$ where $E = E_0 phi^6$ is the energy at rung 6 of the phi-ladder, $h$ is Planck's constant, and $c$ is the speed of light.
background
The module formalizes an RS-coherent photobiomodulation device whose photon energy follows the phi-ladder $E(n) = E_base phi^n$. The therapeutic wavelength is defined by lambda_PBM = planck_h * speed_of_light / E_PBM with E_PBM the rung-6 energy. Upstream lemmas establish the three positivity facts required: planck_h_pos and speed_of_light_pos by direct norm_num, while E_PBM_pos follows from mul_pos applied to phi_pos and eV_to_J_pos.
proof idea
The term proof unfolds the definition of lambda_PBM then applies div_pos to the product of planck_h_pos and speed_of_light_pos over E_PBM_pos.
why it matters
The result supplies the positivity fact needed for the wavelength field inside rs_device, the canonical RS-coherent PBM device whose parameters are derived from the phi-ladder with zero free parameters. It anchors the device to the therapeutic window (750-780 nm) stated in the module documentation and to the eight-tick neutrality constraint on the modulation pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.