dim_M
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assign numerical values or units in terms of τ₀ or ℓ₀.
- Does not derive from the forcing chain T0-T8 or the Recognition Composition Law.
- Does not interact with J-cost, defectDist, or phi-ladder rung calculations.
- Does not specify how mass enters any particular physical equation.
formal statement (Lean)
51def dim_M : Dimension := ⟨0, 0, 1⟩
proof body
Definition body.
52
53/-! ## Physical Constant Dimensions -/
54
55/-- Speed of light dimension: [L¹T⁻¹M⁰] -/