c
plain-language theorem explainer
The definition sets the speed of light to unity in Recognition Science native units, with velocity expressed as voxels per tick. Researchers normalizing equations or scaling quantities on the phi-ladder cite this when working entirely inside the RS system. It is realized as a direct constant assignment carrying the simp attribute for automatic rewriting.
Claim. In the RS-native unit system, the speed of light satisfies $c = 1$, where $c = ℓ_0/τ_0$ with $ℓ_0$ the fundamental length quantum (one voxel) and $τ_0$ the fundamental time quantum (one tick).
background
The module defines a self-contained RS-native measurement system whose base units are the tick (τ₀ = 1, the discrete ledger posting interval) and the voxel (ℓ₀ = 1, the causal spatial step). Velocity is the type alias ℝ for quantities with dimensions of length over time. The upstream RSUnits structure encodes the consistency condition c · τ₀ = ℓ₀, which is satisfied by the present assignment.
proof idea
Direct definition that assigns the literal value 1 to c and attaches the simp attribute; no lemmas or tactics are invoked beyond the built-in constant introduction.
why it matters
This normalization fixes c = 1 as the base gauge for the entire RS framework, enabling all subsequent constants (ħ = φ^{-5}, G = φ^5/π) and the phi-ladder mass formula to be expressed without external anchors. It directly implements the T0–T8 forcing chain requirement that spatial dimensions and the eight-tick octave are measured in units where light traverses one voxel per tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.