SemanticRelation
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not define any operations or morphisms between the constructors.
- Does not prove semantic properties such as transitivity or closure under composition.
- Does not connect the relations to physical constants, the forcing chain, or the Recognition Composition Law.
- Does not address generalizations to other values of configDim.
formal statement (Lean)
15inductive SemanticRelation where
16 | synonymy
17 | antonymy
18 | hypernymy
19 | meronymy
20 | polysemy
21 deriving DecidableEq, Repr, BEq, Fintype
22