speed_of_light
The declaration supplies the exact speed of light in meters per second for wavelength computations in photobiomodulation models. Device physicists applying the φ-energy ladder to therapeutic light sources would cite this value when converting photon energies to wavelengths. It enters as a plain constant definition with no internal reasoning steps.
claimThe speed of light is defined exactly as $299792458$ meters per second.
background
The Photobiomodulation Device module formalizes Recognition Science for light therapy devices coherent with the φ-ladder. It defines discrete energy rungs via $E(n) = E_{base} · φ^n$, where rung 6 yields approximately 1.618 eV corresponding to 766 nm wavelength in the red/near-IR band. The speed of light constant enables conversion from energy to wavelength using $λ = h c / E$, with $h$ from the imported constants module.
proof idea
The definition directly assigns the numerical value 299792458 to the speed of light in real numbers. No lemmas are invoked and no tactics are used; it functions as a fixed constant for downstream expressions.
why it matters in Recognition Science
This constant underpins the lambda_PBM definition and the theorems verifying its placement in the therapeutic window of 750 to 780 nm, as well as the approximation to 766 nm. It bridges the Recognition Science φ-ladder predictions to practical device parameters, supporting the eight-tick octave neutrality in modulation. The declaration addresses the need for SI-unit outputs in applied biophase specifications while the core framework operates in units where c equals 1.
scope and limits
- Does not prove the value from Recognition Science axioms.
- Does not include relativistic or quantum corrections.
- Does not specify the unit system beyond meters per second.
- Does not link to the native RS value of c = 1.
formal statement (Lean)
51def speed_of_light : ℝ := 299792458
proof body
Definition body.
52
53/-- Electron volt to joules conversion, exact -/