syntacticRoleCount
plain-language theorem explainer
The theorem establishes that the syntactic roles defined in the Recognition Science model number exactly five. Linguists deriving universal grammar principles from the configuration dimension would cite this cardinality when building the syntax certificate. The proof is a one-line decision procedure that counts the five constructors of the underlying inductive type.
Claim. The set of syntactic roles consisting of subject, object, predicate, modifier, and complement has cardinality five.
background
The Syntax Universals from ConfigDim module derives syntactic categories from the configuration dimension D = 5 in the Recognition Science framework. This connects Chomsky's universal grammar to the five-dimensional recognition taxonomy of the D = 3 lattice, with the five core phrase structure categories NP, VP, AP, PP, and AdvP matching that dimension. The SyntacticRole inductive type enumerates exactly those five roles: subject, object, predicate, modifier, and complement, and derives the Fintype instance needed for cardinality computations.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype.card expression for the SyntacticRole inductive type. The tactic succeeds because the type has five explicit constructors and the derived Fintype instance supplies the finite enumeration.
why it matters
This cardinality supplies the five_roles field inside the syntaxUniversalsCert definition, which aggregates it with the phrase category count to certify the syntactic universals. It completes the step that forces the role count from configDim D = 5 within the linguistics tier of the framework. The result sits downstream of the SyntacticRole definition and feeds the parent certificate that closes the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.