SemanticRelationsCert
plain-language theorem explainer
SemanticRelationsCert packages the assertion that the enumerated set of lexical-semantic relations has cardinality exactly five. Researchers mapping linguistic structures onto the configDim parameter in Recognition Science would cite the certificate to confirm the D equals five constraint. The declaration is a structure definition whose single field records the Fintype.card result on the inductive enumeration.
Claim. Let $S$ be the inductive type whose constructors are synonymy, antonymy, hypernymy, meronymy, and polysemy. The structure SemanticRelationsCert consists of the single field five_relations asserting that the cardinality of $S$ equals 5.
background
The module establishes five canonical lexical-semantic relations as the content of configDim equals five. These relations are introduced by the inductive type SemanticRelation whose five constructors are synonymy, antonymy, hypernymy, meronymy, and polysemy; the type derives DecidableEq, Repr, BEq, and Fintype so that cardinality statements become computable.
proof idea
The declaration is a structure definition containing one field. The field directly states the equality Fintype.card SemanticRelation = 5, which is discharged by the Fintype instance derived from the inductive definition of SemanticRelation.
why it matters
The certificate is instantiated by the downstream definition semanticRelationsCert, which supplies the concrete value semanticRelation_count. It supplies the linguistic layer of the monolith by fixing the five-relation model at configDim equals five, consistent with the framework's use of configuration dimension to organize semantic spaces beyond the spatial result D equals three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.