`dim_one`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.Dimensions
domain: Constants
line: 42 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.Dimensions on GitHub at line 42.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  39/-! ## Fundamental Dimension Constants -/
  40
  41/-- Dimensionless quantity: [L⁰T⁰M⁰] -/
  42def dim_one : Dimension := ⟨0, 0, 0⟩
  43
  44/-- Length dimension: [L¹T⁰M⁰] -/
  45def dim_L : Dimension := ⟨1, 0, 0⟩
  46
  47/-- Time dimension: [L⁰T¹M⁰] -/
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.