c_eq_one
plain-language theorem explainer
In Recognition Science native units the speed of light is fixed at unity. Workers assembling constant-unification certificates cite this normalization when bundling the alpha bounds and Boltzmann-analog interval. The proof is a direct reflexivity step on the constant definition.
Claim. In Recognition Science native units the speed of light satisfies $c=1$.
background
The declaration belongs to the module supplying calculated proofs for the COMPLETE_PROBLEM_REGISTRY constants. That module records three items: alpha bounded in (0,0.1), c fixed at 1, and the Boltzmann analog k_R bounded in (0,0.5). All proofs employ norm_num, nlinarith and positivity with explicit numerical bounds.
proof idea
The proof is a term-mode reflexivity that matches c directly to the numeral 1. No external lemmas are invoked.
why it matters
The result populates the c_eq_one field of the ConstantsPredictionsCert structure and is referenced by the existence theorem constants_predictions_cert_exists. It supplies the C-005 entry in the registry and anchors the RS-native unit system in which c=1, hbar=phi^{-5} and G=phi^5/pi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.