lambda_PBM_in_therapeutic_window
plain-language theorem explainer
The wavelength derived from the phi-energy ladder at rung 6 satisfies 750 nm < lambda_PBM < 780 nm. Biophysicists and device engineers working in Recognition Science cite this to place the PBM source inside the red/near-IR therapeutic band. The proof unfolds lambda_PBM, invokes positivity of h c, applies the division-bounds lemma on E_PBM, and closes both sides with explicit numerical comparison.
Claim. $750×10^{-9} < hc/ (φ·1.602176634×10^{-19}) < 780×10^{-9}$ (in meters), where $E_{PBM}=φ·eV_to_J$ and $λ_{PBM}=hc/E_{PBM}$ with CODATA values for $h$ and $c$.
background
The module formalizes a photobiomodulation device whose photon energy follows the phi-ladder: $E(n)=E_{base}·φ^n$. E_PBM is defined as phi times the electron-volt-to-joule conversion, so rung 6 yields exactly phi eV. lambda_PBM is then the corresponding wavelength $hc/E_{PBM}$. The therapeutic window 750-780 nm is the interval in which clinical data for red/near-IR efficacy is strongest. div_bounds_of_E_PBM is the upstream lemma that transfers any positive numerator across the fixed E_PBM bounds 1.61 eV_to_J < E_PBM < 1.62 eV_to_J.
proof idea
Unfold lambda_PBM. Establish 0 < planck_h * speed_of_light by mul_pos. Apply div_bounds_of_E_PBM to obtain the two-sided inequality on the quotient. Split the goal with constructor. Close the lower bound by a calc that inserts the numerical lower limit on E_PBM and finishes with norm_num. Close the upper bound symmetrically with the numerical upper limit on E_PBM.
why it matters
The theorem supplies the second key result listed in the module doc-comment, confirming that rung-6 energy lands inside the observed 600-850 nm photobiomodulation band. It is used to populate the wavelength field of the canonical rs_device definition. The result therefore links the Recognition Science phi-ladder (T5-T6) directly to an applied device specification without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.