SemanticRelation
plain-language theorem explainer
The declaration introduces an inductive type with five constructors for the canonical lexical-semantic relations fixed by configDim equal to 5. A formal linguist or Recognition Science modeler would cite it when treating semantic networks as finite types derived from the same dimensional parameter used in physics. The definition proceeds by direct enumeration of the constructors followed by automatic derivation of the required typeclass instances.
Claim. Let $R$ be the inductive type generated by the five constructors synonymy, antonymy, hypernymy, meronymy, and polysemy, equipped with decidable equality, a representation, boolean equality, and finite cardinality.
background
The module Linguistics.SemanticRelationsFromConfigDim identifies five canonical lexical-semantic relations with the configuration dimension D = 5. The relations are synonymy (equivalence of meaning), antonymy (opposition), hypernymy (supertype inclusion), meronymy (part-whole), and polysemy (multiple senses). The local theoretical setting treats semantic structure as fixed by the same dimensional parameter that appears throughout the monolith, with the module documentation stating that these are the five relations equal to configDim D = 5.
proof idea
The declaration is a direct inductive definition that lists the five constructors and derives the instances DecidableEq, Repr, BEq, and Fintype via the deriving clause with no additional lemmas or tactics required.
why it matters
This definition supplies the finite type whose cardinality is certified as exactly 5 by the downstream theorem semanticRelation_count and the structure SemanticRelationsCert. It realizes the linguistic layer by setting configDim D = 5, consistent with the module documentation, and closes the interface between dimensional parameters and semantic relations without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.