SyntaxUniversalsCert
plain-language theorem explainer
SyntaxUniversalsCert packages the two cardinality assertions that the phrase category type and the syntactic role type each contain exactly five elements. Linguists studying universal grammar would cite it to anchor Chomsky-style syntactic principles in the five-dimensional configuration dimension of Recognition Science. The declaration is a bare structure definition that records the Fintype cardinalities of the two inductive enumerations.
Claim. The structure $SyntaxUniversalsCert$ consists of the pair of statements $|PhraseCategory| = 5$ and $|SyntacticRole| = 5$, where $PhraseCategory$ is the inductive type with constructors NP, VP, AP, PP, AdvP and $SyntacticRole$ is the inductive type with constructors subject, object, predicate, modifier, complement.
background
In the Recognition Science treatment of linguistics, syntactic universals are forced by the configuration dimension configDim = 5, which aligns with the five-dimensional recognition taxonomy on the underlying D = 3 spatial lattice. PhraseCategory is the inductive enumeration of the five core phrase-structure categories (NP, VP, AP, PP, AdvP) and automatically carries a Fintype instance from its finite list of constructors. SyntacticRole is the parallel inductive enumeration of the five syntactic roles (subject, object, predicate, modifier, complement) and likewise derives its Fintype instance directly.
proof idea
The declaration is a structure definition with an empty proof body. It simply records the two cardinality equations that follow at once from the Fintype instances already derived on PhraseCategory and SyntacticRole.
why it matters
SyntaxUniversalsCert supplies the certificate consumed by the downstream definition syntaxUniversalsCert, thereby witnessing the syntactic universals required by configDim = 5. It closes the Tier C linguistics layer by connecting Chomsky's universal grammar to the Recognition Science forcing chain at the step where five categories are forced. The construction touches the open question of how the D = 3 lattice projects onto the five-dimensional taxonomy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.