semanticRelation_count
plain-language theorem explainer
The declaration establishes that the inductive type of semantic relations contains exactly five elements, matching the configuration dimension of five in the linguistic extension of Recognition Science. Linguists modeling lexical networks or semantic graphs would cite this when embedding relations into a dimensional framework derived from configDim. The proof is a direct one-line computation of finite type cardinality via the decide tactic.
Claim. The set of semantic relations consisting of synonymy, antonymy, hypernymy, meronymy, and polysemy has cardinality five: $|S| = 5$ where $S = $ {synonymy, antonymy, hypernymy, meronymy, polysemy}.
background
The module treats linguistic semantics as an extension of Recognition Science in which configDim equals five, yielding five canonical lexical-semantic relations. SemanticRelation is the inductive type whose constructors are exactly synonymy, antonymy, hypernymy, meronymy, and polysemy; it derives DecidableEq, Repr, BEq, and Fintype so that cardinality is computable. This rests on the upstream inductive definition of SemanticRelation, which enumerates the relations with no additional hypotheses or axioms.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the goal Fintype.card SemanticRelation = 5. Because the type is finite with five explicit constructors, decide exhaustively verifies the cardinality without further lemmas.
why it matters
The result supplies the five_relations field of semanticRelationsCert, certifying the count inside the linguistics module. It directly instantiates the framework claim that configDim equals five for semantic relations, extending the core Recognition Science structure (spatial dimensions fixed at three via T8) to lexical phenomena. No open questions are addressed; the declaration simply closes the enumeration for downstream certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.