lambda_PBM
plain-language theorem explainer
lambda_PBM defines the therapeutic wavelength in meters for an RS-coherent photobiomodulation device as hc divided by the phi-scaled energy E_PBM. Device modelers working from the phi-energy ladder cite this to fix the source at rung 6. It is realized as a direct noncomputable definition that composes the imported constants without lemmas or reduction steps.
Claim. $λ_{PBM} = hc / E_{PBM}$ (meters), where $E_{PBM} = φ · eV$ is the rung-6 energy on the φ-ladder.
background
The module formalizes an RS-coherent PBM device using the φ-energy ladder. Energies follow E(n) = E_base · φ^n with E_coh = φ^{-5} eV, so rung 6 produces φ eV ≈ 1.618 eV and λ ≈ 766 nm inside the red/near-IR clinical window. The 8-beat modulation pattern satisfies the eight-window neutrality constraint Σ s(k) = 0.
proof idea
This is a one-line definition that directly assembles planck_h, speed_of_light and E_PBM via multiplication and division. No tactics or upstream lemmas are applied.
why it matters
It supplies the wavelength_m field inside the canonical RS device rs_device. Downstream results lambda_PBM_in_therapeutic_window and lambda_PBM_approx place the value inside the 750-780 nm band, while lambda_PBM_pos records positivity. The definition realizes the rung-6 prediction of the φ-ladder and links to the eight-tick octave in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.