Constants Dimensions Dim L

The length dimension

In physics and mathematics, a dimension tells you what kind of quantity a number represents. Length, time, and mass are the three basic kinds. A dimension is not a unit: meters and feet are both units of the same dimension, length. The declaration dim_L is the formal name for that dimension inside the Recognition Science framework's machine-checked library of formal theorems.

Concretely, dim_L is defined as a triple of integers, written [L¹T⁰M⁰]. The first entry is the length exponent, set to 1. The second and third entries, time and mass, are set to 0. This triple says: a quantity with this dimension is a length, nothing more and nothing less. The same library defines dim_T as [L⁰T¹M⁰] for time and dim_M as [L⁰T⁰M¹] for mass, and dim_one as [L⁰T⁰M⁰] for dimensionless numbers.

The point of the triple is to keep calculations honest. When the framework multiplies two dimensioned quantities, it adds the exponents; when it divides, it subtracts them. The speed of light, for instance, carries dimension [L¹T⁻¹M⁰], length over time. The reduced Planck constant carries [L²T⁻¹M¹], and Newton's gravitational constant carries [L³T⁻²M⁻¹]. These signatures let the library check that a formula like the Planck length, √(ħG/c³), really does come out with dimension [L¹], as a length should.

In Recognition Science, the framework models the fundamental units as a tick τ₀, the atomic time quantum, and a recognition length ℓ₀ defined as c·τ₀. The dimension structure is the bookkeeping that keeps those units consistent when physical constants are derived from them. The declaration dim_L is the anchor of that bookkeeping for length: it is the label attached to any quantity the framework treats as a length.

What dim_L does not do is set a scale. It does not say how long anything is, and it does not pick meters or feet or any other unit. It only fixes the kind of quantity. The numerical value of a length lives elsewhere, in a separate structure that pairs a real number with its dimension. The dimension tells you what the number means; the number tells you how much.

/-- Length dimension: [L¹T⁰M⁰] -/
def dim_L : Dimension := ⟨1, 0, 0⟩

/-- Time dimension: [L⁰T¹M⁰] -/
def dim_T : Dimension := ⟨0, 1, 0⟩

/-- Mass dimension: [L⁰T⁰M¹] -/
def dim_M : Dimension := ⟨0, 0, 1⟩

/-- 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

dim_L does not assign any numerical value or unit to a length. The dimension structure alone does not derive the speed of light or any other constant. No claim is made here about how many spatial dimensions the framework forces.

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: