Constants Dimensions Dim Hbar

The dimensions of action

The reduced Planck constant, written ℏ and pronounced h-bar, is the quantum of angular momentum. It carries the physical dimensions of action: energy multiplied by time, or equivalently momentum multiplied by length. In the SI system those dimensions are kilogram meters squared per second. The constant's value is about 1.054571817 × 10⁻³⁴ joule-seconds, a measurement tied to the 2019 redefinition of SI base units.

Dimensional analysis tracks how physical quantities combine by recording their exponents in length, time, and mass. A speed has dimensions L¹T⁻¹, an acceleration L¹T⁻², a force M¹L¹T⁻². The reduced Planck constant has the signature L²T⁻¹M¹: two powers of length, one inverse power of time, one power of mass. That signature is what makes ℏ the natural unit for angular momentum and for the action integrals of quantum mechanics.

The framework's machine-checked library, a collection of formal theorems verified by computer, defines this signature explicitly. Its declaration dim_hbar sets the dimension of ℏ to the triple ⟨2, -1, 1⟩, meaning length squared, inverse time, and mass. This is a definitional choice, not a proved theorem. The same library defines matching signatures for the speed of light, the gravitational constant, and the fundamental tick of recognition time. These signatures let the library verify that Planck's length, time, and mass formulas are dimensionally consistent: the square root of ℏG/c³ has the dimensions of length, and the analogous expressions for time and mass check out.

What dim_hbar does not claim is just as important as what it establishes. It does not derive the numerical value of ℏ. It does not prove that action is quantized, nor that angular momentum comes in discrete units. It only records the dimensional fingerprint of the constant, so that later calculations in the library can check their own consistency. The declaration is a piece of bookkeeping, not a law of physics.

The payoff is that dimensional consistency becomes a formal guarantee rather than a hand calculation. When the library builds Planck units or recognition-time expressions, it can verify by machine that every product and quotient carries the correct exponents. That is a modest but real service: it catches sign errors and misplaced powers before they propagate into larger derivations.

/-- Reduced Planck constant dimension: [L²T⁻¹M¹] -/
def dim_hbar : Dimension := ⟨2, -1, 1⟩

/-- Reduced Planck constant dimension: [L²T⁻¹M¹] -/
def dim_hbar : Dimension := ⟨2, -1, 1⟩

/-- Speed of light dimension: [L¹T⁻¹M⁰] -/
def dim_c : Dimension := ⟨1, -1, 0⟩

/-- Gravitational constant dimension: [L³T⁻²M⁻¹] -/
def dim_G : Dimension := ⟨3, -2, -1⟩

/-- Reduced Planck constant dimension: [L²T⁻¹M¹] -/
def dim_hbar : Dimension := ⟨2, -1, 1⟩

What this page does not claim

No derivation of the numerical value of ℏ is claimed. No proof that action or angular momentum is quantized is claimed. No claim that the dimensional signature alone determines any physical law is made.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/Dimensions.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: