dim_c
plain-language theorem explainer
dim_c supplies the dimensional exponents for the speed of light as length to the first power, time to the minus first, and mass to the zero. Researchers normalizing constants inside the Recognition Science framework cite it when verifying homogeneity of derived quantities such as ħ and G. The entry is a direct record construction that populates the three integer fields of Dimension.
Claim. The speed of light is assigned the dimensional signature $[L^{1}T^{-1}M^{0}]$, with the three integers denoting the exponents of length, time, and mass.
background
The module supplies a dimensional analysis framework built on the Recognition Science primitives τ₀ (fundamental tick), ℓ₀ = c·τ₀ (recognition length), and φ (golden ratio scaling factor). Every physical quantity receives a signature [L^a, T^b, M^c] that records the exponents of length, time, and mass. The Dimension structure is the record type carrying exactly these three integer fields together with decidable equality.
proof idea
Direct definition that applies the anonymous constructor to the Dimension structure, supplying the concrete integers 1, -1, and 0.
why it matters
The definition fixes the dimensional signature of c, which is normalized to 1 in RS-native units. It participates in the self-consistent derivation of the remaining constants (ħ = φ^{-5}, G = φ^5/π) and supports the mass formula on the phi-ladder. No immediate downstream theorems are recorded, yet the entry closes part of the dimensional bookkeeping required by the eight-tick octave and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.