lambda_PBM_approx
plain-language theorem explainer
The theorem shows that the photobiomodulation wavelength from rung 6 of the φ-energy ladder satisfies |λ_PBM - 766 nm| < 5 nm. Device designers working on RS-coherent light therapy would cite it to locate the operating point inside the red/near-IR window. The proof unfolds the wavelength definition, pulls bounds from the energy interval via a division lemma, checks numerical references with norm_num, and closes the absolute-value inequality with linear arithmetic.
Claim. $|λ_{PBM} - 766×10^{-9}| < 5×10^{-9}$ (in meters), where $λ_{PBM} = hc / E_{PBM}$ and $E_{PBM}$ is the photon energy at rung 6 of the φ-ladder (approximately 1.618 eV).
background
The module formalizes an RS-coherent photobiomodulation device built on the φ-energy ladder $E(n) = E_{base} · φ^n$. Rung 6 yields $E = φ$ eV, so the therapeutic wavelength is defined by $λ_{PBM} = planck_h · speed_of_light / E_{PBM}$. The module documentation states that this places the device inside the 600–850 nm band where clinical evidence is strongest and that the accompanying 8-beat modulation pattern satisfies eight-window neutrality Σ s(k) = 0.
proof idea
Unfolds the definition of λ_PBM. Establishes positivity of planck_h · speed_of_light. Invokes div_bounds_of_E_PBM to transfer the energy interval (1.61–1.62 eV) into wavelength bounds. Verifies the reference inequalities at 761 nm and 771 nm by norm_num. Applies lt_trans twice and finishes with abs_lt.mpr together with linarith.
why it matters
It supplies the concrete numerical anchor for the therapeutic wavelength at rung 6, confirming the module’s key result that E(6) ≈ φ eV maps to λ ≈ 766 nm. The result supports the device specification in RS_Biophase_Light_Device_Spec.tex and links the φ-ladder to the eight-tick octave and strain-neutral modulation. No downstream theorems yet reference it, so it functions as a terminal approximation claim inside the applied photobiomodulation section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.