lambda_PBM_in_therapeutic_window
plain-language theorem explainer
The wavelength lambda_PBM derived from the phi-energy ladder at rung 6 satisfies 750 nm < lambda_PBM < 780 nm. Modelers of RS-coherent photobiomodulation devices cite this result to place the device output inside the red/near-IR therapeutic band. The proof unfolds the wavelength definition, invokes a division-bounds lemma on E_PBM, and closes the two inequalities by direct numerical comparison.
Claim. $750 < 10^9 lambda < 780$ where $lambda = hc / E$ and $E = phi * 1.602176634 * 10^{-19}$ J.
background
The module formalizes an RS-coherent photobiomodulation device whose photon energy follows the phi-ladder E(n) = E_base * phi^n. E_PBM is defined as phi * eV_to_J, the energy at rung 6. lambda_PBM is then hc / E_PBM with h and c the standard constants. The upstream lemma div_bounds_of_E_PBM states that for any positive K the quotient K / E_PBM lies strictly between K / (1.62 eV_to_J) and K / (1.61 eV_to_J).
proof idea
Unfold lambda_PBM. Establish positivity of planck_h * speed_of_light by mul_pos. Apply div_bounds_of_E_PBM to obtain the sandwich. Use constructor to split the conjunction, then two calc blocks that compare the explicit numerical bounds 750e-9 and 780e-9 via norm_num.
why it matters
The result anchors the therapeutic wavelength inside the module's phi-ladder construction and supplies the wavelength field of the downstream rs_device definition. It realizes the explicit prediction that rung 6 yields approximately 766 nm, consistent with the eight-tick octave and the alpha-band constants of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.