c_eq_one'
plain-language theorem explainer
The speed of light is normalized to unity in Recognition Science native units. Researchers computing dimensionless couplings such as alpha_G cite this normalization to simplify expressions involving G, hbar, and c. The proof is a single reflexivity step that matches the unit convention directly.
Claim. In Recognition Science native units the speed of light satisfies $c=1$.
background
The module computes the dimensionless gravitational coupling alpha_G := G m_e^2 / (hbar c) using Constants.G, Constants.hbar, Constants.c and the electron structural mass. In these units the expression reduces to a closed phi-form. The module doc states that the raw RS-native value is O(10^9) while the SI target is O(10^{-45}), marking the row as a hypothesis bridge that requires an explicit dimensional map.
proof idea
The proof is a one-line reflexivity that directly equates c to the native-unit value 1.
why it matters
This supplies the c=1 normalization applied by the downstream theorem hbar_c_eq_hbar. It implements the RS-native unit choice (c=1, hbar=phi^{-5}, G=phi^5/pi) that lets alphaG_pred_eq close the phi-form. The open question it touches is the explicit ExternalCalibration map needed to reach CODATA numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.