PhraseCategory
plain-language theorem explainer
The inductive definition enumerates the five core phrase categories NP, VP, AP, PP, and AdvP. Linguists studying universal grammar in the Recognition Science setting would cite it to tie syntactic structure to configDim = 5. It is realized as a direct enumeration that automatically derives Fintype for cardinality results.
Claim. Let $C$ be the set of phrase categories with elements NP (noun phrase), VP (verb phrase), AP (adjective phrase), PP (prepositional phrase), and AdvP (adverb phrase).
background
The module Syntax Universals from ConfigDim treats syntactic categories as forced by the Recognition Science configuration dimension equal to 5. This matches the five core phrase structure categories listed in the module documentation. The definition supplies the finite set needed to equate phrase count with the 5-dimensional recognition taxonomy of the D=3 lattice.
proof idea
The declaration is a direct inductive definition of the five constructors, followed by derivation of DecidableEq, Repr, BEq, and Fintype instances.
why it matters
This definition supplies the type for the downstream theorems phraseCategoryCount and SyntaxUniversalsCert, which certify that both phrase categories and syntactic roles have cardinality 5. It occupies the linguistic tier of the framework by anchoring universal grammar to configDim = 5 and the D=3 lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.