pith. sign in
module module high

IndisputableMonolith.Constants.Dimensions

show as:
view Lean formalization →

The Dimensions module supplies a type for dimensional signatures using exponents of length, time, and mass to track units in calculations. Researchers deriving constants from Recognition Science primitives would cite it to enforce dimensional homogeneity. It defines the Dimension type together with base vectors dim_L, dim_T, dim_M and a status indicator. The module is a pure definition block with no proofs.

claimA dimension signature is a triple of integers $(l,t,m)$ giving the exponents of length, time and mass. The module supplies the neutral element $(0,0,0)$ and the three base dimensions $(1,0,0)$, $(0,1,0)$, $(0,0,1)$.

background

The module sits inside the Recognition Science development and imports the parent Constants module, whose sole documented content is the fundamental RS time quantum τ₀ = 1 tick. It introduces the Dimension type whose purpose is to carry the signature [Length, Time, Mass] exponents so that later calculations can verify dimensional consistency. The sibling definitions dim_one, dim_L, dim_T, dim_M and dimensions_status are the concrete objects that realize this tracking.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module is imported by IndisputableMonolith.Constants.Derivation, whose documentation records the CODATA reference values for c, ℏ and G and states that constants are derived from Recognition Science primitives. It therefore supplies the dimensional bookkeeping required for any unit-consistent derivation of those constants.

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)