CategoryConcept
plain-language theorem explainer
An inductive type enumerates the five canonical category theory primitives fixed by the configuration dimension parameter equal to five. Researchers formalizing Recognition Science's mathematical depth layer would cite this enumeration when specifying the categorical constructs required by configDim. The definition is a direct inductive listing of the five constructors together with automatically derived instances for decidable equality and finite cardinality.
Claim. Let $C$ be the inductive type whose five constructors are the canonical category-theoretic primitives: object, morphism, functor, natural transformation, and limit/colimit.
background
The module defines category theory concepts as a finite collection of five elements determined by the configuration dimension D = 5. These primitives are the standard building blocks of category theory: object, morphism, functor, natural transformation, and limit or colimit. The local theoretical setting is the mathematical depth section of Recognition Science, where configDim fixes the number of such constructs needed before further categorical developments.
proof idea
The declaration is the inductive definition of the type with exactly five constructors, together with the derived instances DecidableEq, Repr, BEq, and Fintype.
why it matters
This definition supplies the type whose cardinality is shown to equal five by the downstream cardinality theorem and is packaged inside the certification structure of the same module. It directly realizes the module statement that configDim D = 5 corresponds to these five category theory constructs. In the Recognition framework it anchors the categorical layer that precedes further developments such as the certificate structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.