SyntacticRole
plain-language theorem explainer
The inductive definition enumerates five syntactic roles as subject, object, predicate, modifier, and complement. Linguists extending Recognition Science to Tier C syntax would cite it when linking universal grammar to configDim = 5. It is a direct inductive enumeration that derives Fintype to enable immediate cardinality results.
Claim. The syntactic roles form the finite set consisting of subject, object, predicate, modifier, and complement.
background
The module treats syntactic universals as forced by configDim D = 5, matching the five phrase-structure categories NP, VP, AP, PP, AdvP. These roles correspond to the 5-dimensional recognition taxonomy of the underlying D = 3 lattice. The setting follows the Recognition Science claim that syntactic categories arise directly from the configuration dimension rather than from separate linguistic axioms.
proof idea
The declaration is an inductive definition with five explicit constructors that automatically derives the DecidableEq, Repr, BEq, and Fintype instances.
why it matters
This definition supplies the five roles required by SyntaxUniversalsCert, which records that both PhraseCategory and SyntacticRole have cardinality 5. It implements the module claim that syntactic universals follow from configDim D = 5 and connects to the Recognition Science forcing chain in which D = 3 determines higher-dimensional structures. The construction closes one step in the Tier C linguistics scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.