Constants Dimensions Positive Dimensioned Quantity

A positive dimensioned quantity

In physics and engineering, a dimensioned quantity pairs a real number with a unit, such as 3 meters or 1.5 seconds. The number alone is incomplete: 3 means little until you know it is 3 meters, not 3 kilograms. Dimensional analysis tracks how these units combine when quantities are multiplied, divided, or raised to powers, and it is the standard tool for checking whether an equation is even plausible before solving it.

Within the Recognition Science framework, the machine-checked library of formal theorems defines a ledger, a discrete record of recognition events, as the primitive from which physical constants are derived. To handle those constants cleanly, the framework first builds a small dimensional algebra. A dimension is a triple of integers recording the exponents of length, time, and mass: the speed of light gets [1, -1, 0], the reduced Planck constant gets [2, -1, 1], and the gravitational constant gets [3, -2, -1]. A dimensioned quantity then pairs a real value with one of these triples.

The declaration PositiveDimensionedQuantity adds one constraint: the value must be strictly greater than zero. This is a definitional choice, not a derived theorem. It models the fact that physical constants such as the speed of light, the reduced Planck constant, and the gravitational constant are all positive real numbers. The framework uses this type to carry those constants through calculations, and it provides multiplication, division, and square root operations that combine both the values and the dimension exponents correctly.

What the declaration does not do is give any constant its numerical value. It does not prove that the speed of light is 299,792,458 meters per second, nor does it derive the reduced Planck constant or the gravitational constant from first principles. Those derivations, where they exist, live elsewhere in the framework. PositiveDimensionedQuantity is the container, not the content: it says a physical constant is a positive number with a dimensional signature, and it leaves the actual number to other parts of the library.

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

/-- A dimensioned physical quantity with its value and dimensional signature. -/
structure DimensionedQuantity where
  value : ℝ
  dim : Dimension

/-- A positive dimensioned quantity (for physical constants). -/
structure PositiveDimensionedQuantity extends DimensionedQuantity where
  value_pos : 0 < value

What this page does not claim

This declaration does not assign numerical values to any physical constant. This declaration does not prove that the speed of light, the reduced Planck constant, or the gravitational constant are positive; it merely requires it as a definitional constraint. This declaration does not establish the dimensional signatures of the constants; those are separate definitions.

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: