lambda_PBM_approx
plain-language theorem explainer
The theorem establishes that the Recognition Science photobiomodulation wavelength at rung 6 satisfies |λ_PBM − 766 nm| < 5 nm. Device physicists working from the phi-ladder would reference this bound for red/near-IR therapy specifications. The tactic proof unfolds the wavelength definition, invokes positivity of Planck's constant and speed of light, applies a division-bounds lemma, and closes with numerical comparisons and linear arithmetic.
Claim. $|λ_{PBM} - 766 × 10^{-9}| < 5 × 10^{-9}$, where $λ_{PBM} = h c / E_{PBM}$ and $E_{PBM}$ satisfies $1.61$ eV $< E_{PBM} < 1.62$ eV (converted via the exact eV-to-joule factor).
background
The PhotobiomodulationDevice module formalizes an RS-coherent light therapy device. It defines the phi-energy ladder by $E(n) = E_{base} · φ^n$ with $E_{coh} = φ^{-5}$ eV, so rung 6 produces $E(6) = φ$ eV. The therapeutic wavelength is the definition lambda_PBM := planck_h * speed_of_light / E_PBM. The module also records an 8-beat modulation pattern $s(k) = cos(kπ/4) + (1/φ)·cos(kπ/2)$ whose eight-window sum is exactly zero. Upstream, div_bounds_of_E_PBM states that for any positive K the inequalities K/(1.62 eV_to_J) < K/E_PBM < K/(1.61 eV_to_J) hold once E_PBM_bounds are given; planck_h_pos and speed_of_light_pos supply the required positivity facts.
proof idea
Unfold lambda_PBM. Form the positivity fact 0 < planck_h * speed_of_light by mul_pos on the two positivity lemmas. Apply div_bounds_of_E_PBM to obtain the wavelength sandwich. Establish the reference bounds (761e-9 < hc/(1.62 eV_to_J)) and (hc/(1.61 eV_to_J) < 771e-9) by norm_num on the constants. Chain the inequalities by lt_trans, then close with abs_lt.mpr and two linarith applications.
why it matters
This supplies the concrete numerical anchor for the therapeutic-wavelength claim in the module documentation, confirming that rung-6 energy lands inside the 600-850 nm clinical window. It closes the applied-physics specification for the RS-coherent PBM device using only CODATA values for h and c together with the phi-ladder. No downstream theorems depend on it; the result stands as a verified bound supporting direct application of the phi-ladder (T5-T6) to biophotonics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.