dimensionalAnalysisCert
plain-language theorem explainer
The definition supplies a concrete certificate that the SI base quantities consist of five primary ones whose count is five and that seven total quantities partition as five plus two. A physicist working in Recognition Science would cite it when grounding dimensional analysis in the configDim D = 5 structure. The construction is a direct record that assembles the two decided theorems into the required structure fields.
Claim. The structure $DimensionalAnalysisCert$ requires that the finite set of base quantities has cardinality five and that seven equals five plus two. The definition $dimensionalAnalysisCert$ is the instance that satisfies the first requirement by the count of primary quantities and the second by the explicit partition of the seven SI bases.
background
In the Recognition Science treatment of dimensional analysis, the SI system is decomposed into seven base quantities. Five of these (length, mass, time, electric current, temperature) are treated as primary and kinematic or dynamic, matching the configuration dimension of five. The remaining two (amount of substance and luminous intensity) are auxiliary and derivable from the five via mole and photon counts. The structure $DimensionalAnalysisCert$ encodes this split by requiring that the finite type of base quantities has cardinality five and that seven equals five plus two. The upstream theorem baseQuantity_count establishes the cardinality five by direct decision, while si_partition confirms the arithmetic split seven equals five plus two.
proof idea
The definition is a one-line wrapper that directly supplies the theorem baseQuantity_count to the five_primary field and the theorem si_partition to the si_split field of the DimensionalAnalysisCert structure.
why it matters
This definition populates the DimensionalAnalysisCert structure that anchors the dimensional analysis layer in the Recognition Science framework. It directly implements the statement from the module documentation that five quantities are primary and kinematic/dynamic corresponding to configDim D = 5. No downstream uses are recorded yet, but it closes the basic count for the five-primary split that feeds higher-level physics derivations such as the mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.