pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Constants.Dimensions

show as:
view Lean formalization →

The Dimensions module supplies type-level tracking for physical dimensions via exponent triples for length, time, and mass. It equips downstream derivations with DimensionedQuantity and PositiveDimensionedQuantity to enforce unit consistency when computing RS constants. Physicists working on the phi-ladder mass formula or the eight-tick octave would reference these definitions to maintain dimensional homogeneity. The module contains only definitions and no theorems.

claimA dimension is a triple of integer exponents $(l,t,m)$ for length, time, and mass. A dimensioned quantity is a pair consisting of a numerical value and its dimension $D$.

background

This module sits inside the Constants hierarchy and imports the base RS time quantum τ₀ = 1 tick from IndisputableMonolith.Constants. It introduces Dimension as the signature [Length, Time, Mass] exponents, along with specific instances dim_L, dim_T, dim_M, dim_c, dim_hbar, dim_G. DimensionedQuantity and PositiveDimensionedQuantity wrap values with these dimensions to track physical units through calculations. The local setting follows the Recognition Science framework where constants are expressed in phi-native units with c=1, ħ=φ^{-5}, G=φ^5/π.

proof idea

This is a definition module, no proofs. It declares the Dimension type and its constructors, then defines the standard basis dimensions and the dimensioned quantity wrappers.

why it matters in Recognition Science

The definitions here feed directly into the Constants.Derivation module, which derives physical constants from Recognition Science primitives using CODATA references for c, ħ, and G. It supports the overall forcing chain by ensuring dimensional consistency in the T5 J-uniqueness and T8 D=3 spatial dimensions steps.

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)