def
definition
dim_G
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.Dimensions on GitHub at line 62.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
87τ₀ = √(ℏG/(πc³))/c has dimension [T]:
88 [√(ℏG/c³)/c] = [L¹]/[L¹T⁻¹] = [T¹] ✓
89-/
90
91/-! ## Dimensioned Quantities -/
92