CategoryTheoryCert
plain-language theorem explainer
CategoryTheoryCert records that Recognition Science produces exactly five categorical structures. Researchers formalizing RS categorically would cite it to confirm the match with configDim D = 5. The declaration is a structure definition that sets the field five_structures to the Fintype cardinality of the inductive type CategoricalStructure.
Claim. The structure asserts that the finite cardinality of the enumerated set of canonical categorical structures equals five: $ |{objects, morphisms, functors, natural transformations, adjunctions}| = 5 $.
background
The module states that five canonical categorical structures equal configDim D = 5. Recognition maps act as functors that preserve J-cost structure, and the Yoneda lemma embeds the recognition field in the functor category. The sibling inductive type CategoricalStructure enumerates the five constructors objects, morphisms, functors, naturalTransformations, adjunctions and derives a Fintype instance.
proof idea
Direct structure definition. The single field five_structures is declared as the equality Fintype.card CategoricalStructure = 5, using the derived Fintype instance on the inductive type.
why it matters
The definition is instantiated by the downstream categoryTheoryCert in the same module and by the parallel CategoryTheoryCert in CategoryTheoryConceptsFromConfigDim. It supplies the categorical count that aligns with the module's claim of five structures for D = 5, supporting the interpretation of recognition maps as functors within the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.