si_partition
plain-language theorem explainer
This theorem asserts that the seven SI base quantities equal five primary kinematic quantities plus two derived auxiliaries. It is cited when constructing the dimensional analysis certificate that aligns Recognition Science configDim with the SI system. The proof is a one-line decision procedure verifying the arithmetic identity.
Claim. The seven SI base quantities satisfy $7 = 5 + 2$, where the five primary quantities are the kinematic and dynamic set (length, mass, time, electric current, temperature) and the two are auxiliary (amount of substance, luminous intensity).
background
The module frames the SI system as having seven base quantities. Five are primary kinematic and dynamic quantities tied to configDim equal to five: length, mass, time, electric current, temperature. The two auxiliaries (amount-of-substance and luminous-intensity) are presented as derivable from the primary set via mole and photon counts. This establishes a direct correspondence between Recognition Science's config dimension and standard SI units with zero axioms or sorrys.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the numerical equality.
why it matters
This theorem supplies the si_split field inside the dimensionalAnalysisCert definition, which certifies the mapping from the five primary quantities (configDim = 5) to the full SI base set. It supports the framework's separation of primary versus auxiliary quantities and contributes to the forcing chain grounding dimensional structure in observable units, consistent with the eight-tick octave and the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.