BaseQuantity
plain-language theorem explainer
An inductive enumeration defines the five primary base quantities in the Recognition Science treatment of dimensional analysis. A physicist verifying dimensional homogeneity in equations or reducing SI units to the configDim framework would reference this list. The definition proceeds by listing the five cases and deriving the standard typeclass instances for equality and finiteness.
Claim. Let $B$ denote the finite set of primary base quantities consisting of length, mass, time, electric current, and temperature, equipped with decidable equality, a representation, boolean equality, and a Fintype structure.
background
The module frames seven SI base quantities, of which five are primary and correspond to configDim $D=5$ in Recognition Science: length, mass, time, electric current, and temperature. The remaining two (amount-of-substance and luminous intensity) are treated as auxiliary and derivable via mole and photon counts. Temperature enters via the upstream definition as the inverse of the Lagrange multiplier beta, satisfying the thermodynamic relation $dE/dS = T$.
proof idea
The declaration is a direct inductive definition that enumerates five constructors and derives DecidableEq, Repr, BEq, and Fintype via the deriving clause.
why it matters
This enumeration supplies the domain for the theorem baseQuantity_count establishing cardinality 5 and for the structure DimensionalAnalysisCert that records the SI split as 5 + 2. It anchors the Recognition Science reduction of physics to five kinematic/dynamic dimensions, consistent with the configDim $D=5$ setting and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.