speed_of_light_pos
The lemma asserts that the speed of light constant is strictly positive. Modelers of photobiomodulation devices cite it to guarantee that wavelength and energy conversions remain well-defined on the positive reals. The proof is a direct one-line norm_num reduction on the explicit numerical definition.
claim$0 < c$ where $c = 299792458$ denotes the speed of light in meters per second.
background
The module formalizes Recognition Science foundations for a photobiomodulation device that operates on the phi-energy ladder. Key definitions include the discrete energy rungs E(n) = E_base · phi^n and the therapeutic wavelength derived from rung 6, which yields approximately 766 nm in the red/near-IR window. The constant speed_of_light is introduced as the exact real number 299792458 to support Planck-constant multiplications in wavelength formulas.
proof idea
One-line wrapper that applies the norm_num tactic directly to the definition of speed_of_light.
why it matters in Recognition Science
The result supplies the positivity hypothesis required by the three downstream theorems lambda_PBM_pos, lambda_PBM_in_therapeutic_window, and lambda_PBM_approx. Those theorems establish that the derived wavelength lies inside the 750-780 nm therapeutic band and satisfies the 8-window neutrality constraint of the Recognition Science framework. It therefore closes the positivity step in the phi-ladder energy-to-wavelength pipeline.
scope and limits
- Does not derive the numerical value of c from Recognition Science axioms.
- Does not incorporate relativistic or quantum-field corrections.
- Applies only inside the real-number model of device parameters.
- Does not address dimensional consistency beyond the given definition.
Lean usage
have h_hc_pos : 0 < planck_h * speed_of_light := mul_pos planck_h_pos speed_of_light_posformal statement (Lean)
57lemma speed_of_light_pos : 0 < speed_of_light := by norm_num [speed_of_light]