speed_of_light
plain-language theorem explainer
This definition supplies the exact numerical value of the speed of light in meters per second for use in photobiomodulation calculations. Device designers and biophysics modelers cite it when computing wavelengths from the φ-energy ladder. The definition is a direct constant assignment with no computation or lemmas required.
Claim. We define the speed of light by $c := 299792458$ (in meters per second).
background
The Photobiomodulation Device module formalizes Recognition Science foundations for light therapy operating in coherence with the φ-ladder. It defines discrete energy rungs via $E(n) = E_{base} · φ^n$, identifies rung 6 as yielding approximately 1.618 eV, and computes the corresponding wavelength near 766 nm inside the red/near-IR therapeutic window. The module also requires an 8-beat modulation pattern that satisfies 8-window neutrality to avoid accumulation of recognition strain.
proof idea
This is a direct constant definition that assigns the numerical value 299792458 to the speed of light. No tactics or lemmas are applied.
why it matters
This definition feeds the wavelength computations in lambda_PBM, lambda_PBM_approx, and lambda_PBM_in_therapeutic_window. It supplies the physical constant c needed to connect the φ-energy ladder to observable wavelengths inside the 750-780 nm window. The placement aligns with the module's emphasis on RS-coherent light therapy and the eight-tick neutrality constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.