semanticRelation_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the five relations from the forcing chain T0-T8 or the Recognition Composition Law.
- Does not prove that these relations are exhaustive outside the given inductive definition.
- Does not connect the relations to physical constants, the phi-ladder, or Berry creation thresholds.
- Does not show how configDim equals five follows from upstream Recognition Science axioms.
Lean usage
example : Fintype.card SemanticRelation = 5 := semanticRelation_countformal statement (Lean)
23theorem semanticRelation_count : Fintype.card SemanticRelation = 5 := by decide
proof body
24