Dimension
plain-language theorem explainer
The Dimension structure supplies the type for tracking physical quantities by integer exponents on length, time, and mass. Researchers deriving constants or forcing spatial dimensions in Recognition Science cite it when composing dimensional signatures. It is supplied directly as a structure definition carrying decidable equality on the triple.
Claim. A dimension is a triple of integers $(L,T,M)$ that records the exponents in the monomial form $[length^L time^T mass^M]$.
background
Recognition Science starts from the fundamental tick τ₀, recognition length ℓ₀ = c τ₀, and golden ratio φ. Every quantity is assigned a dimensional signature [L^a T^b M^c] to maintain unit consistency across derivations. The module imports Length, Time, and Mass as real numbers from RSNativeUnits and the spatial Dimension abbrev from DimensionForcing, which records the forced value 3.
proof idea
Structure definition that directly declares the three integer fields and derives decidable equality. No lemmas or tactics are invoked; the declaration itself supplies the type used by all later dimensioned quantities.
why it matters
This supplies the common type for dim_c, dim_hbar, and dim_G, which in turn feed the theorems spatial_dims_eq_3 and eight_tick_forces_temporal in CurvatureSpaceDerivation. It implements the bookkeeping required by T8 of the forcing chain, where D = 3 spatial dimensions is obtained from the eight-tick octave. The same type appears in balance_from_conservation and config_space_is_5D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.