speed_of_light_pos
plain-language theorem explainer
The lemma establishes strict positivity of the speed of light constant in SI units. Modelers deriving photobiomodulation wavelengths cite it to guarantee that products and quotients involving Planck's constant remain positive. The proof is a one-line numerical normalization that evaluates the constant definition directly.
Claim. Let $c = 299792458$ denote the speed of light in meters per second. Then $0 < c$.
background
The Photobiomodulation Device module formalizes Recognition Science foundations for light therapy coherent with the φ-ladder. Photon energies follow the discrete rungs E(n) = E_base · φ^n, and wavelengths are obtained from λ = h c / E. The upstream definition supplies the exact SI value 299792458 for speed_of_light, which enters all subsequent positivity and bounding arguments.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to the definition of speed_of_light, confirming the numerical inequality holds.
why it matters
It supplies the positivity fact required by the three downstream theorems lambda_PBM_pos, lambda_PBM_in_therapeutic_window and lambda_PBM_approx. Those results place the computed wavelength inside the 750-780 nm therapeutic window, realizing the module's claim that rung 6 of the φ-ladder yields a photon energy near 1.618 eV and a wavelength near 766 nm.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.