syntacticRoleCount
plain-language theorem explainer
The theorem states that the syntactic roles form a finite type of cardinality exactly five. Linguists modeling universal grammar from configDim would cite it to ground the five roles in the Recognition Science taxonomy. The proof is a one-line decision procedure on the derived Fintype instance.
Claim. The set of syntactic roles has cardinality five: $|S| = 5$, where $S$ consists of subject, object, predicate, modifier, and complement.
background
The module treats syntactic universals as forced by configDim D=5, which yields the five core phrase structure categories and corresponds to the five-dimensional recognition taxonomy of the underlying D=3 lattice. SyntacticRole is defined as the inductive type with exactly those five constructors and derives DecidableEq, Repr, BEq, and Fintype instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance of SyntacticRole.
why it matters
The result supplies the five_roles component of syntaxUniversalsCert, which certifies both phrase categories and roles. It fills the linguistic tier of the module's claim that syntactic structure follows from configDim D=5, extending the Recognition Science framework beyond the spatial D=3 case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.