dim_one
plain-language theorem explainer
The declaration supplies the zero-exponent triple for dimensionless quantities in the Recognition Science dimensional framework. Researchers deriving constants from τ₀ and ℓ₀ would invoke it to strip units from ratios. The definition is a direct instantiation of the Dimension structure with all exponents set to zero.
Claim. The dimensionless dimension is the triple $(0,0,0)$ in the space of length, time, and mass exponents.
background
Recognition Science employs a dimensional signature [L^a T^b M^c] for each quantity, as defined by the Dimension structure whose fields record the integer exponents for length, time, and mass. This module builds a framework starting from fundamental units τ₀ (tick), ℓ₀ (recognition length), and φ (golden ratio) to derive constants self-consistently. The upstream Dimension definition provides the carrier type for these signatures, while the separate spatial Dimension from DimensionForcing tracks the number of spatial dimensions forced by the eight-tick octave.
proof idea
It is a direct definition that constructs the Dimension record with L, T, and M all equal to zero.
why it matters
This definition establishes the neutral element for dimensional multiplication in the Recognition Science constants module. It supports the derivation of physical constants by allowing dimensionless combinations, consistent with the overall program of obtaining ℏ, G, and c from Recognition primitives. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.