def
definition
dim_M
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.Dimensions on GitHub at line 51.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
48def dim_T : Dimension := ⟨0, 1, 0⟩
49
50/-- Mass dimension: [L⁰T⁰M¹] -/
51def dim_M : Dimension := ⟨0, 0, 1⟩
52
53/-! ## Physical Constant Dimensions -/
54
55/-- Speed of light dimension: [L¹T⁻¹M⁰] -/
56def dim_c : Dimension := ⟨1, -1, 0⟩
57
58/-- Reduced Planck constant dimension: [L²T⁻¹M¹] -/
59def dim_hbar : Dimension := ⟨2, -1, 1⟩
60
61/-- Gravitational constant dimension: [L³T⁻²M⁻¹] -/
62def dim_G : Dimension := ⟨3, -2, -1⟩
63
64/-! ## Dimensional Consistency (Documentation)
65
66The Planck length formula has correct dimensions:
67 ℓ_P = √(ℏG/c³)
68 [ℏG/c³] = [L²T⁻¹M¹][L³T⁻²M⁻¹]/[L³T⁻³M⁰]
69 = [L⁵T⁻³M⁰]/[L³T⁻³M⁰]
70 = [L²T⁰M⁰]
71 [√(ℏG/c³)] = [L¹] ✓
72
73The Planck time formula has correct dimensions:
74 t_P = √(ℏG/c⁵)
75 [ℏG/c⁵] = [L²T⁻¹M¹][L³T⁻²M⁻¹]/[L⁵T⁻⁵M⁰]
76 = [L⁵T⁻³M⁰]/[L⁵T⁻⁵M⁰]
77 = [L⁰T²M⁰]
78 [√(ℏG/c⁵)] = [T¹] ✓
79
80The Planck mass formula has correct dimensions:
81 m_P = √(ℏc/G)