syntaxUniversalsCert
plain-language theorem explainer
Linguists applying Recognition Science to syntax cite this definition for the certificate that exactly five phrase categories and five syntactic roles exist. It follows from the configuration dimension being five, matching the recognition taxonomy of the D=3 lattice. The definition assembles the two decide-proved cardinality theorems into the required structure.
Claim. The certificate structure holds when the cardinality of the phrase category type equals five and the cardinality of the syntactic role type equals five.
background
The module develops Tier C linguistics within Recognition Science, reinterpreting Chomsky's universal grammar as a consequence of the configuration dimension equaling five. Phrase categories comprise the five standard types: noun phrases, verb phrases, adjective phrases, prepositional phrases, and adverb phrases. Syntactic roles consist of subject, object, predicate, modifier, and complement. These enumerations are certified by the upstream theorems phraseCategoryCount and syntacticRoleCount, each established by the decide tactic on the finite type definitions. The five-dimensional count aligns with the recognition taxonomy of the underlying three-dimensional lattice.
proof idea
The definition constructs the required structure by assigning the theorem phraseCategoryCount to the five_phrases field and syntacticRoleCount to the five_roles field. No additional reasoning is performed; the proof body consists solely of these two field assignments.
why it matters
This provides the explicit certificate realizing the syntactic universals forced by configDim = 5. It populates the structure whose fields are the two cardinality statements. In the broader framework it links the T8-derived spatial dimension D = 3 to linguistic structure through the five-dimensional recognition taxonomy. No parent theorems or downstream applications are recorded, leaving open its integration into larger derivations of semantic or pragmatic universals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.