DimensionedQuantity
plain-language theorem explainer
DimensionedQuantity pairs a real scalar with an integer triple of length, time, and mass exponents to track physical quantities under dimensional analysis. Researchers deriving constants from Recognition Science primitives or checking consistency in nucleosynthesis tiers cite it when scaling quantities along the phi-ladder. The declaration is a direct structure definition with two fields and no proof obligations.
Claim. A dimensioned quantity consists of a real value together with a dimensional signature given by a triple of integers recording the exponents of length, time, and mass.
background
The module supplies a dimensional analysis framework for Recognition Science built on the primitives tau_0 (fundamental tick), ell_0 = c tau_0 (recognition length), and phi (geometric scaling factor). Every physical quantity carries a signature [L^a, T^b, M^c]. The sibling Dimension structure records these three integer exponents and is used to track how quantities transform under multiplication or scaling. Upstream results from NucleosynthesisTiers establish that physical quantities occupy discrete phi-tiers, for example nuclear density scaling as phi^n times Planck density.
proof idea
This declaration is a structure definition introducing the type of dimensioned quantities; no lemmas are applied and no reduction steps occur.
why it matters
DimensionedQuantity supplies the carrier type used by dimensions_status to summarize the module and by PositiveDimensionedQuantity to impose positivity for physical constants. It supports derivation of dimensions for c, hbar, and G from the fundamental tick and recognition length, consistent with the eight-tick octave and D=3 in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.