pith. machine review for the scientific record. sign in
def definition def or abbrev high

semanticRelationsCert

show as:
view Lean formalization →

This definition assembles a certificate structure that records the exact count of five lexical-semantic relations for the linguistics component of Recognition Science. Framework users working on semantic dimensionality would cite it to confirm that the relation set matches configDim D equals 5. The construction proceeds by direct assignment of the cardinality established by an upstream decision theorem.

claimLet $C$ be the structure whose field requires that the finite cardinality of the semantic relation type equals five. The certificate is the instance of $C$ in which this field is set to the value of the theorem establishing that the cardinality equals five.

background

Recognition Science assigns configDim equal to five in its linguistics module to capture five canonical lexical-semantic relations: synonymy, antonymy, hypernymy, meronymy, and polysemy. An upstream theorem proves by decision procedure that the finite cardinality of the semantic relation type is exactly five. The certificate structure is defined to hold precisely this cardinality assertion.

proof idea

This is a one-line definition that populates the certificate structure by assigning the result of the cardinality theorem to its sole field.

why it matters in Recognition Science

The definition provides the concrete witness for the five-relation count demanded by the linguistics depth, completing the module's zero-sorry status. It supports derivations that tie lexical structures to the five-dimensional configDim, consistent with the framework's forcing chain where dimensions are fixed by self-similar fixed points and octaves. No immediate parent theorems are listed, leaving open its integration into larger semantic proofs.

scope and limits

formal statement (Lean)

  28def semanticRelationsCert : SemanticRelationsCert where
  29  five_relations := semanticRelation_count

proof body

Definition body.

  30
  31end IndisputableMonolith.Linguistics.SemanticRelationsFromConfigDim

depends on (2)

Lean names referenced from this declaration's body.