dim_M
plain-language theorem explainer
Mass dimension is the signature with length and time exponents zero and mass exponent one. Researchers deriving physical constants from Recognition Science primitives reference it when tracking mass scaling in equations. The definition is a direct constructor application to the Dimension record.
Claim. The mass dimension is defined as the triple $⟨0, 0, 1⟩$ in the Dimension structure, corresponding to $[L^0 T^0 M^1]$.
background
The Dimension structure records integer exponents for length (L), time (T), and mass (M) in a triple, equipped with decidable equality. This module establishes a dimensional analysis framework for Recognition Science, starting from the fundamental tick τ₀, recognition length ℓ₀ = c τ₀, and golden ratio φ, from which constants ħ, G, and c are derived self-consistently. The upstream Dimension definition supplies the record type used here and in sibling constants such as dim_L and dim_T.
proof idea
One-line definition that constructs the Dimension value with L=0, T=0, M=1.
why it matters
This definition supplies the mass signature required by the dimensional analysis framework for deriving physical constants from Recognition Science primitives. It supports the module's goal of expressing ħ, G, and c via dimensional signatures and aligns with the overall use of [L^a T^b M^c] triples to track scaling on the phi-ladder. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.