c_rs_eq_one
Establishes that the speed of light equals 1 in RS-native units. Researchers deriving Planck-scale quantities or forcing spacetime emergence from the Recognition Science foundation cite this normalization step. The proof is a direct term-mode reduction that unfolds the ratio definition and applies numerical simplification.
claimIn RS-native units the speed of light satisfies $c_{rs} = 1$, where $c_{rs}$ is defined as the ratio of the fundamental length scale to the fundamental time scale.
background
The ConstantDerivations module derives the fundamental constants from the RS foundation via the Composition Law and the J-cost function. The speed of light is introduced as the ratio $c_{rs} := ℓ_0 / τ_0$, with $ℓ_0$ the unit length and $τ_0$ the eight-tick fundamental period. In the native unit system both scales are fixed to 1, so the ratio collapses to unity by construction of causal coherence.
proof idea
The term-mode proof unfolds the definition of $c_{rs}$ together with the definitions of $ℓ_0$ and $τ_0$, then invokes norm_num to reduce the resulting numerical expression to 1.
why it matters in Recognition Science
The result is invoked by all_constants_from_phi to list every constant as an algebraic function of φ, by planck_length_eq_one and planck_mass_eq to normalize Planck units, and by the master theorems reality_forced_by_any_distinction and reality_from_one_distinction to close the forcing chain. It realizes the Level-4 step of the derivation diagram in the module documentation, fixing the causal bound at unity after the eight-tick octave and three-dimensional forcing steps.
scope and limits
- Does not recover the laboratory value of c in SI units.
- Does not derive c from experimental data or additional physical postulates.
- Holds only after the choice of RS-native units where ℓ_0 = τ_0 = 1.
- Does not address propagation in curved recognition geometry.
Lean usage
theorem c_pos : c_rs > 0 := by rw [c_rs_eq_one]; norm_numformal statement (Lean)
105theorem c_rs_eq_one : c_rs = 1 := by
proof body
Term-mode proof.
106 unfold c_rs ℓ₀ τ₀
107 norm_num
108
109/-- c > 0. -/