c
plain-language theorem explainer
The definition assigns the exact SI value 299792458 to the speed of light in meters per second. Analysts needing to compare Recognition Science mass ladders or alpha predictions against laboratory data would import this quarantined constant. The implementation is a direct noncomputable assignment carrying the simp attribute.
Claim. The speed of light is the real number $c = 299792458$ (exact SI definition, in m/s).
background
The module isolates empirical SI/CODATA constants from the certified Recognition Science surface so that the top-level certificate chain and its import closure remain independent of numeric inputs. The upstream definition supplies a constant scalar field via constant (c : ℝ) : ScalarField := { ψ := fun _ => c }. Sibling declarations in the same module provide the corresponding values for hbar and G together with their positivity and nonzeroness facts.
proof idea
One-line definition that directly binds the integer 299792458 to the real number c.
why it matters
This supplies the reference value for c when numeric comparisons are required, while keeping the main forcing chain (T0-T8), Recognition Composition Law, and phi-ladder derivations independent of empirical inputs. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.