Constants Dimensions Dimension

The Dimension record

In physics, a dimension is a label for how a quantity scales with the basic measures of length, time, and mass. Speed, for instance, scales as length divided by time, so its dimension is written [L¹T⁻¹M⁰]. The Recognition Science framework encodes this familiar idea as a small data structure called Dimension: a record holding three integers, one for the exponent of length, one for time, and one for mass. The declaration itself is a definition, not a formal proof. It chooses a representation, it does not prove a fact about nature.

The framework then uses this record to assign dimensions to the constants it works with. The speed of light gets [L¹T⁻¹M⁰], the reduced Planck constant gets [L²T⁻¹M¹], and the gravitational constant gets [L³T⁻²M⁻¹]. These match the standard assignments from conventional physics. The same record supports a small algebra: multiplying two dimensioned quantities adds their exponents, dividing subtracts them, and taking a square root halves them. The framework's documentation uses this algebra to check that the Planck length, time, and mass formulas have the correct dimensions, and that its fundamental tick τ₀ has dimension [T]. These checks are worked examples, not new physical laws.

In Recognition Science, the framework's own units start from a fundamental tick of time and a recognition length equal to the speed of light times that tick. The Dimension record is the bookkeeping that keeps those units consistent as the framework derives constants such as ℏ and G. What the declaration does not do is establish that space has three dimensions, that the constants have the values they do, or that any particular physical theory is true. It only fixes the notation for talking about dimensions inside the machine-checked library of formal statements. The physical content of the framework lives in other declarations that build on this bookkeeping.

/-- Dimensional signature: [Length, Time, Mass] exponents.
    Used to track physical dimensions through calculations. -/
structure Dimension where
  L : ℤ  -- Length exponent
  T : ℤ  -- Time exponent
  M : ℤ  -- Mass exponent
  deriving DecidableEq

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

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

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

What this page does not claim

The Dimension declaration does not establish that physical space has three dimensions. The Dimension declaration does not assign numerical values to the constants c, ℏ, or G. The Dimension declaration does not prove that the Planck unit formulas are physically correct.

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: