Pith. sign in
module module high

IndisputableMonolith.Constants.Dimensions

show as:
view Lean formalization →

The Dimensions module supplies the dimensional signature as a triple of integer exponents for Length, Time, and Mass. Researchers working on constant derivations in Recognition Science cite it to maintain unit consistency across calculations. It is a definition module with no proofs, importing the base Constants module that sets the RS time quantum.

claimA dimensional signature is a triple $(l,t,m) \in \mathbb{Z}^3$ recording the exponents of length, time, and mass for any physical quantity.

background

The module sits inside the Recognition Science framework and imports the base Constants module whose sole documented fact is the fundamental RS time quantum $\tau_0 = 1$ tick. It introduces the type Dimension together with concrete instances dim_one, dim_L, dim_T, dim_M, dim_c, dim_hbar, and dim_G that label the standard basis vectors in the three-dimensional exponent space.

The local theoretical setting is the need to track how quantities combine under multiplication and division while preserving dimensional homogeneity, exactly as required when constants such as $c$, $\hbar$, and $G$ are later expressed in RS-native units.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the dimensional bookkeeping required by the downstream Derivation module, whose documented purpose is to obtain the physical constants $c$, $\hbar$, and $G$ from Recognition Science primitives and to compare them with CODATA reference values.

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)