syntaxUniversalsCert
plain-language theorem explainer
The definition assembles two cardinality results into a certificate asserting exactly five phrase categories and five syntactic roles. Linguists examining universal grammar or Recognition Science researchers mapping configDim D=5 to syntax would cite it. It is a direct structure constructor that pairs the two decide lemmas as field values.
Claim. Let $P$ be the finite type of phrase categories and $R$ the finite type of syntactic roles. The definition supplies a witness to the structure requiring $|P|=5$ and $|R|=5$.
background
The module treats syntactic universals as forced by configDim D=5 in the Recognition Science setting. Five core phrase-structure categories (NP, VP, AP, PP, AdvP) are identified with this dimension and linked to the five-dimensional recognition taxonomy of the underlying D=3 lattice. PhraseCategory is the type whose cardinality is proved equal to 5 by the upstream theorem phraseCategoryCount. SyntacticRole is the type whose cardinality is proved equal to 5 by syntacticRoleCount. Both upstream results are obtained by the decide tactic.
proof idea
The definition is a one-line wrapper that supplies the theorems phraseCategoryCount and syntacticRoleCount directly as the two fields of the SyntaxUniversalsCert structure.
why it matters
The definition supplies the concrete certificate for the module claim that syntactic universals arise from configDim D=5. It thereby connects the Recognition Science D=3 lattice taxonomy to linguistic phrase structure. No parent theorems or downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.