pith. sign in
module module high

IndisputableMonolith.Constants.Dimensions

show as:
view Lean formalization →

This module defines the dimensional signature used to track physical quantities in Recognition Science constants. It supplies the type Dimension as the triple of integer exponents for length, time, and mass, together with named instances for the base dimensions and for c, ℏ, G. The module is imported by Constants.Derivation to enforce dimensional consistency during constant derivations from RS primitives. It contains only definitions and instances, with no theorems or proofs.

claimDimension is the type $\mathbb{Z}^3$ whose components are the exponents of length, time, and mass. The module also defines the specific dimensions $\mathrm{dim}_L = (1,0,0)$, $\mathrm{dim}_T = (0,1,0)$, $\mathrm{dim}_M = (0,0,1)$, $\mathrm{dim}_c = (1,-1,0)$, $\mathrm{dim}_{\hbar} = (2,-1,1)$, $\mathrm{dim}_G = (3,-2,-1)$, together with the wrapper types DimensionedQuantity and PositiveDimensionedQuantity.

background

The parent module IndisputableMonolith.Constants introduces the fundamental RS time quantum $\tau_0 = 1$ tick. The Dimensions submodule extends this foundation by supplying a uniform way to record how any derived quantity scales under changes of the three base units.

It defines Dimension as the signature $[L,T,M]$ of integer exponents and provides the named constants dim_one, dim_L, dim_T, dim_M, dim_c, dim_hbar, dim_G. The wrapper types DimensionedQuantity and PositiveDimensionedQuantity attach these signatures to numeric values.

The module therefore supplies the notational and type-level machinery needed to keep all subsequent constant derivations dimensionally homogeneous.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the dimensional bookkeeping required by IndisputableMonolith.Constants.Derivation. That downstream module derives the numerical values of c, ℏ, and G from RS primitives while referencing the CODATA reference values; the Dimension type guarantees that each step preserves the correct $[L,T,M]$ signature.

It therefore occupies the position immediately after the basic Constants module and immediately before any derivation that must remain dimensionally consistent.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)