SyntacticRole
plain-language theorem explainer
SyntacticRole enumerates the five core syntactic roles in phrase structure. Linguists modeling universal grammar via the Recognition Science configDim D=5 constraint would cite this enumeration as the forced categories. The declaration is a direct inductive definition that automatically derives decidable equality and finite cardinality.
Claim. The syntactic roles form the finite set consisting of subject, object, predicate, modifier, and complement.
background
The module reinterprets Chomsky's universal grammar in Recognition Science terms, where syntactic categories are forced by configDim D=5. The five core phrase structure categories (NP, VP, AP, PP, AdvP) equal this dimension and map to the 5-dimensional recognition taxonomy of the D=3 lattice. The declaration supplies the roles that pair with the five phrase categories in the certification structure.
proof idea
This is a direct inductive definition of the five roles, with automatic derivation of DecidableEq, Repr, BEq, and Fintype.
why it matters
The definition supplies the five roles used by the downstream syntacticRoleCount theorem and the SyntaxUniversalsCert structure to certify that both phrase categories and roles number five. It fills the D=5 slot required by the configDim forcing in the module, aligning syntactic universals with the 5-dimensional taxonomy of the D=3 lattice. No open questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.