c_rs_eq_one
plain-language theorem explainer
The theorem establishes that the speed of light equals unity in Recognition Science native units. Researchers normalizing constants derived from the J-cost function and phi-ladder cite this result when setting the causal bound. The proof is a direct unfolding of the definition as the ratio of fundamental length to time followed by numerical simplification.
Claim. In Recognition Science native units, where the fundamental length and fundamental time are each set to 1, the speed of light satisfies $c = 1$.
background
Recognition Science derives constants from the J-cost function satisfying the Recognition Composition Law, with the self-similar fixed point phi emerging as the unique solution, followed by the eight-tick period and three spatial dimensions. The module derives the fundamental time as eight ticks and the fundamental length as the unit length, so the speed of light is the ratio of these two quantities.
The upstream definition states that the speed of light is the ratio of fundamental length to fundamental time, and in native units where both equal 1 this ratio is 1. This choice implements the causal bound that nothing propagates faster than one unit of length per unit of time.
proof idea
The proof unfolds the definition of the speed of light as the ratio of fundamental length to fundamental time and applies norm_num to reduce the resulting expression to equality with 1.
why it matters
This supplies the normalization c = 1 used in the theorem all_constants_from_phi, which assembles c = 1 together with hbar equal to a power of phi and G equal to a power of phi. It is invoked in the proofs of c positivity, Planck length equal to 1, and Planck mass equal to phi to the minus five. The result realizes the level-4 step of the derivation chain in the module, where the speed of light is obtained as the ratio of fundamental length to fundamental time after the forcing chain has fixed phi and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
DBI scalar fields tie ΛCDM on late-time data, H₀ near 73
"H0 = 73.29 ± 0.16 km/s/Mpc (Model I) ... H0 ≈ 73.0 ± 1.0 km/s/Mpc late universe"
-
"Weak null singularity survives a relativistic fluid"
"p = p(τ), 0 < p' < 1 ... Under the assumption that p' < 1, the sound cones lie strictly inside the light cones."