dim_L
plain-language theorem explainer
The declaration defines the length dimension as the exponent triple with unit length and zero time and mass components. Researchers assigning units to derived quantities such as position or wavelength in Recognition Science cite this when composing dimensional signatures. It is a direct constructor application of the Dimension structure.
Claim. The length dimension is the signature $[L^1 T^0 M^0]$.
background
The module supplies a dimensional analysis framework for Recognition Science in which every quantity carries a signature $[L^a T^b M^c]$ tracking length, time, and mass exponents. The Dimension structure encodes these exponents as integers L, T, M with decidable equality. This setting rests on the primitives τ₀ (fundamental tick) and ℓ₀ = c · τ₀ together with the geometric scaling factor φ, from which constants ℏ, G, and c are derived self-consistently.
proof idea
Direct definition that applies the Dimension structure constructor to the integer triple 1, 0, 0.
why it matters
This definition supplies the canonical length signature used to label all length-bearing quantities in the constants module. It supports the self-consistent derivation of physical constants from Recognition Science units described in the module documentation. No downstream theorems are recorded for this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.