SemanticRelationsCert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the five relations from the J-uniqueness or Recognition Composition Law.
- Does not address whether further relations appear in empirical language data.
- Does not link the relations to mass formulas or physical constants.
- Does not prove that the set remains fixed when configDim changes.
formal statement (Lean)
25structure SemanticRelationsCert where
26 five_relations : Fintype.card SemanticRelation = 5
27