categoricalStructureCount
plain-language theorem explainer
The theorem establishes that exactly five categorical structures arise in the recognition framework. A researcher formalizing category theory within physics would cite this count to confirm the dimension of the categorical layer. The proof is a direct decision procedure that evaluates the cardinality of the inductive type with five explicit constructors.
Claim. The finite set of categorical structures has cardinality five, consisting of objects, morphisms, functors, natural transformations, and adjunctions: $|CategoricalStructure| = 5$.
background
Recognition Science derives category theory from J-cost preservation under recognition maps, which function as functors. The module states that five canonical structures (objects, morphisms, functors, natural transformations, adjunctions) equal configDim D = 5, with the recognition field embedded via the Yoneda lemma. The upstream inductive definition enumerates these five cases and derives Fintype, DecidableEq, and related instances.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic computes Fintype.card directly from the five constructors of the inductive type CategoricalStructure.
why it matters
The result populates the five_structures field of categoryTheoryCert, certifying the categorical layer in the Recognition Science mathematics module. It realizes the module claim that five structures match configDim D = 5 and sits downstream of the J-cost and recognition composition law machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.