PhraseCategory
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the five categories from the J-uniqueness equation or phi fixed point.
- Does not address cross-linguistic exceptions or parameter settings.
- Does not link phrase categories to physical constants or mass ladder formulas.
formal statement (Lean)
18inductive PhraseCategory where
19 | NP | VP | AP | PP | AdvP
20 deriving DecidableEq, Repr, BEq, Fintype
21