SyntaxUniversalsCert
plain-language theorem explainer
SyntaxUniversalsCert records the two cardinality assertions that establish exactly five phrase categories and five syntactic roles. Linguists applying Recognition Science to universal grammar would cite it when mapping configDim D=5 onto syntactic structure. The declaration is a structure definition whose fields are the direct Fintype.card equalities supplied by the two inductive enumerations.
Claim. Let $P$ be the inductive type with five constructors NP, VP, AP, PP, AdvP and $R$ the inductive type with five constructors subject, object, predicate, modifier, complement. Then SyntaxUniversalsCert is the structure whose fields assert that the cardinality of $P$ equals 5 and the cardinality of $R$ equals 5.
background
The module treats syntactic universals as consequences of configDim D=5 in the Recognition Science framework, where this dimension corresponds to the five-dimensional recognition taxonomy of the underlying D=3 lattice. PhraseCategory is the inductive type whose constructors are exactly the five core phrase-structure categories NP, VP, AP, PP, AdvP. SyntacticRole is the inductive type whose constructors are the five roles subject, object, predicate, modifier, complement. Both derive their Fintype instances directly from the inductive definitions, so their cardinalities are fixed at five by construction.
proof idea
The declaration is a structure definition. Its two fields are literal equalities Fintype.card PhraseCategory = 5 and Fintype.card SyntacticRole = 5; no lemmas or tactics are invoked because the Fintype instances are supplied automatically by the inductive declarations of the two types.
why it matters
The structure is the type of the witness constructed by syntaxUniversalsCert, which supplies the concrete certification that the five phrase categories and five roles are forced by configDim D=5. It therefore occupies the step that translates the Recognition Science forcing chain (T8 D=3 lattice) into a linguistic universal-grammar claim. The module notes that this matches Chomsky's proposal once the dimensional count is imposed by the recognition taxonomy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.