pith. machine review for the scientific record. sign in
def definition def or abbrev high

c_rs

show as:
view Lean formalization →

Researchers deriving physical constants from the Recognition Science foundation cite this definition for the speed of light. It sets c_rs to the ratio of fundamental length ell_0 to fundamental time tau_0. In native units where both are unity, this enforces c=1 as a statement of causal coherence rather than a free parameter. The definition follows directly from the unit normalization in the forcing chain.

claimIn RS-native units the speed of light is defined by $c = ell_0 / tau_0$, with $ell_0$ the fundamental length and $tau_0$ the fundamental time.

background

The Constant Derivations module derives c, hbar, G, and alpha from the RS foundation rather than as free parameters. The chain begins with the Composition Law, defines the J-cost J(x) = 1/2(x + 1/x) - 1, forces phi as the self-similar fixed point, sets D = 3, and fixes tau_0 to eight ticks with ell_0 the matching unit length. This definition expresses c as the ratio ell_0 over tau_0.

proof idea

The declaration is a direct noncomputable definition assigning c_rs to the quotient ell_0 / tau_0. No lemmas are applied; it is the base assignment that later theorems unfold to prove equals 1.

why it matters in Recognition Science

It is referenced by the theorem all_constants_from_phi that asserts c_rs = 1 together with hbar = phi^{-5} and G = phi^5. The module documentation places it at Level 4 of the derivation chain. It supports the subsequent definitions of Planck length and mass that reduce to 1 and phi^{-5} in native units, confirming consistency with the eight-tick octave and phi-ladder.

scope and limits

formal statement (Lean)

 102noncomputable def c_rs : ℝ := ℓ₀ / τ₀

proof body

Definition body.

 103
 104/-- c = 1 in RS-native units. -/

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.