def
definition
dim_c
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Constants.Dimensions on GitHub at line 56.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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)
82 [ℏc/G] = [L²T⁻¹M¹][L¹T⁻¹M⁰]/[L³T⁻²M⁻¹]
83 = [L³T⁻²M¹]/[L³T⁻²M⁻¹]
84 = [L⁰T⁰M²]
85 [√(ℏc/G)] = [M¹] ✓
86