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

E_PBM

show as:
view Lean formalization →

The photobiomodulation energy is defined as the golden ratio multiplied by the electron-volt to joule conversion factor. Device modelers in Recognition Science cite this value when fixing the sixth rung on the phi-energy ladder for light therapy calculations. The declaration is a direct noncomputable definition that performs the multiplication.

claimThe photobiomodulation energy equals the golden ratio times the electron-volt-to-joule conversion factor, yielding a photon energy of approximately 1.618 eV.

background

The module defines the phi-energy ladder by E(n) = E_base · phi^n with coherent base E_coh = phi^{-5} eV, so that rung 6 produces exactly phi eV. The upstream definition supplies the exact conversion factor 1.602176634e-19 from electron volts to joules. This local setting supports RS-coherent light therapy whose wavelength is predicted to fall inside the 600-850 nm therapeutic band.

proof idea

The declaration is a direct definition that multiplies the golden ratio constant by the electron-volt conversion factor.

why it matters in Recognition Science

Downstream results including the bounds lemma, the rung-6 identity theorem, and the wavelength definition all depend on this value. It supplies the explicit rung-6 energy step in the module's phi-ladder description, linking to the eight-tick octave and therapeutic-window claims in the Recognition Science framework.

scope and limits

formal statement (Lean)

  99noncomputable def E_PBM : ℝ := phi * eV_to_J

proof body

Definition body.

 100

used by (7)

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

depends on (1)

Lean names referenced from this declaration's body.