baseQuantity_count
plain-language theorem explainer
Recognition Science dimensional analysis relies on the fact that exactly five primary base quantities exist, as encoded by the finite type BaseQuantity. This count is invoked by the dimensionalAnalysisCert to separate primary from auxiliary SI quantities. The proof reduces to a single decide application that exploits the Fintype derivation from the five-constructor inductive definition.
Claim. The cardinality of the type of primary base quantities equals five: $|B| = 5$ where $B = $ {length, mass, time, electric current, temperature}.
background
In the module on dimensional analysis from config dimension, the SI system is framed with seven base quantities, of which five are treated as primary in Recognition Science: length, mass, time, electric current, and temperature. The inductive definition BaseQuantity lists precisely these five constructors, each deriving DecidableEq, Repr, BEq, and Fintype. This setup aligns with the upstream result that configDim equals five for the kinematic and dynamic sector, separating the two auxiliary quantities (amount of substance and luminous intensity) as derivable.
proof idea
The proof is a one-line term that invokes the decide tactic on the equality Fintype.card BaseQuantity = 5. Because BaseQuantity is a finite inductive type with five constructors, Lean’s Fintype instance computes the cardinality by enumeration, and decide discharges the goal by reflexivity after normalization.
why it matters
This cardinality result supplies the five_primary field in the downstream DimensionalAnalysisCert definition, which certifies the split between primary and auxiliary quantities. It directly supports the Recognition Science claim that five dimensions suffice for the core physics before introducing the spatial dimension D=3 and the phi-ladder mass formulas. The result closes a small but necessary bookkeeping step in the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.