phraseCategoryCount
plain-language theorem explainer
The theorem establishes that the inductive type of phrase categories has cardinality five. Linguists working in Recognition Science would cite it to ground universal grammar in the five-dimensional configuration space. The proof is a one-line decision procedure that confirms the Fintype cardinality by enumerating the five constructors.
Claim. The set of phrase categories has cardinality five: $|$NP, VP, AP, PP, AdvP$| = 5$.
background
In the Syntax Universals from ConfigDim module, syntactic categories are forced by the configuration dimension fixed at D = 5. The PhraseCategory inductive type enumerates the five core phrase structures: noun phrase (NP), verb phrase (VP), adjective phrase (AP), prepositional phrase (PP), and adverb phrase (AdvP). This corresponds to the five-dimensional recognition taxonomy of the D = 3 spatial lattice in the Recognition Science framework.
proof idea
The proof is a one-line wrapper that applies the decide tactic to Fintype.card PhraseCategory = 5. The tactic succeeds because PhraseCategory derives Fintype, allowing direct enumeration of the five cases to verify the cardinality.
why it matters
This theorem supplies the five_phrases field in the SyntaxUniversalsCert definition, which certifies the syntactic universals. It fills the linguistic tier by grounding the five categories in configDim D = 5, connecting to the Recognition Science forcing chain where spatial dimensions are fixed at three. It touches the open question of mapping these categories onto the phi-ladder or eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.