pith. machine review for the scientific record. sign in
def definition def or abbrev high

lambda_PBM

show as:
view Lean formalization →

The definition computes the therapeutic wavelength for an RS-coherent photobiomodulation device as the ratio of Planck's constant times the speed of light to the PBM energy fixed at φ eV. Biophysicists and device engineers working inside the Recognition Science framework cite it when specifying the operating wavelength of φ-ladder light therapy. The definition is a direct algebraic substitution of the module constants with no additional lemmas required.

claim$λ_{PBM} := hc / E_{PBM}$ where $E_{PBM} = φ · (1 eV)$ converted to joules.

background

The Photobiomodulation Device module formalizes an RS-coherent light therapy device built on the φ-energy ladder. Energies follow E(n) = E_base · φ^n with the biophase scale E_coh = φ^{-5} eV; rung 6 therefore yields E_PBM = φ eV. The constants planck_h and speed_of_light are the exact CODATA values for h and c. The definition converts this energy into the corresponding wavelength in meters.

proof idea

One-line definition that substitutes the product of planck_h and speed_of_light divided by E_PBM.

why it matters in Recognition Science

This definition supplies the wavelength parameter for the canonical RS-coherent device rs_device and feeds the downstream theorems that locate the wavelength inside the 750-780 nm therapeutic window and the tighter 766 nm approximation. It realizes the concrete device prediction from the φ-ladder (rung 6) inside the Recognition Science framework and closes the link between abstract energy rungs and applied hardware specifications.

scope and limits

formal statement (Lean)

 142noncomputable def lambda_PBM : ℝ := planck_h * speed_of_light / E_PBM

proof body

Definition body.

 143

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.