categoryTheoryCert
plain-language theorem explainer
The definition supplies a certificate that the configuration dimension D equals five yields precisely five category-theoretic primitives. Researchers tracing how Recognition Science parameters recover standard category theory would reference it to confirm the enumerated count. It is realized as a direct abbreviation that populates the five_concepts field of CategoryTheoryCert with the decidable cardinality result.
Claim. Let $C$ be the finite type enumerating the five category concepts. The structure CategoryTheoryCert is instantiated by setting its field five_concepts to the equality $|C| = 5$.
background
The module fixes the configuration dimension at D = 5 and identifies the five canonical constructs as object, morphism, functor, natural transformation, and limit or colimit. The upstream theorem categoryConcept_count proves by direct decision that Fintype.card CategoryConcept equals five. CategoryTheoryCert is the structure whose single field records this cardinality equality.
proof idea
This is a one-line wrapper that constructs the CategoryTheoryCert instance by assigning the theorem categoryConcept_count directly to the five_concepts field.
why it matters
The certificate closes the local count for category concepts under configDim D = 5 and is referenced by the parallel construction in CategoryTheoryFromRS. It supports the claim that Recognition Science recovers the standard five core notions when the dimension parameter is five. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.