c_ell0_tau0
plain-language theorem explainer
The light-cone identity equates the fundamental length unit ℓ₀ to the product of the speed of light c and the fundamental time unit τ₀ in RS-native units. Researchers constructing RSUnits structures or proving kinematic invariants cite this lemma when rescaling observables. The proof reduces immediately to the definitions via a single simplification step.
Claim. In RS-native units, $c · τ₀ = ℓ₀$, where $c$ is the speed of light, $τ₀$ the duration of one tick, and $ℓ₀$ the fundamental voxel length.
background
The Constants module sets the fundamental time quantum as tick := 1, with τ₀ defined as an abbreviation for tick. The length unit ℓ₀ is defined as 1, and c follows the same native-unit convention. This establishes the convention in which the speed of light equals unity. Upstream, the tick definition supplies the RS time quantum, while the Derivation module expresses τ₀ and ℓ₀ via codata relations involving ħ, G, and c.
proof idea
The proof is a one-line term proof that applies simp to the definitions of c, tau0, ell0, and tick, collapsing both sides of the equality to 1.
why it matters
This identity populates the RSUnits structure used for unit-independent calculations. Downstream lemmas in KDisplay, such as ell0_div_tau0_eq_c and K_gate_units_invariant, apply it to prove invariance of observables under rescaling. It realizes the light-cone relation required by the eight-tick octave and consistent scaling on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.