HasConfigDim5
plain-language theorem explainer
HasConfigDim5 asserts that a finite type has cardinality exactly 5. Cross-domain theorems in Recognition Science cite it to record that five independent realizations (sensory, emotional, biological, economic, linguistic) each carry this cardinality. The definition is a direct abbreviation of the Fintype.card equality.
Claim. Let $T$ be a finite type. Then $T$ satisfies config dim 5 precisely when $|T|=5$.
background
Module C13 formalizes the structural claim that config dim D=5 appears across the framework with high frequency. The predicate HasConfigDim5 supplies the basic building block: a type is declared to have this dimension exactly when it is finite and has five elements. The module then records five concrete instances and derives equicardinality and triple-product results from them.
proof idea
The declaration is a definition that directly equates the predicate to the cardinality condition on finite types.
why it matters
It is the common antecedent for the five domain-specific theorems (sensory_hasConfigDim5 through linguistic_hasConfigDim5) and for ConfigDimUniversalityCert, which packages one instance from each domain. The module doc positions the predicate as the first of four steps that establish D=5 universality; the downstream equicardinal and product theorems rest on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.