pith. machine review for the scientific record. sign in
module module low

IndisputableMonolith.Linguistics.SemanticRelationsFromConfigDim

show as:
view Lean formalization →

This module defines semantic relations in linguistics derived from configuration dimension within the Recognition Science framework. It introduces SemanticRelation as the core type, along with count and certification functions, building directly on the imported Constants module. The module supplies basic linguistic objects parameterized by config dim for later use in semantic analysis. Its structure consists entirely of definitions and type declarations with no embedded proofs.

claimThe module defines the type $SemanticRelation$ over configuration dimensions together with the functions $semanticRelation_count : SemanticRelation → ℕ$ and $SemanticRelationsCert$ providing certification.

background

The upstream Constants module supplies the fundamental RS time quantum τ₀ = 1 tick. This linguistics module extends that foundation by introducing configuration dimension as the parameter governing semantic structures. SemanticRelation captures relations between semantic entities indexed by config dim, while the sibling declarations semanticRelation_count and SemanticRelationsCert supply cardinality and certification mechanisms. The module imports only Mathlib and Constants, keeping all definitions local to the linguistics domain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the basic semantic objects that higher-level linguistic constructions in Recognition Science would reference. It extends the core RS constants (τ₀ and the forcing chain) into the linguistics domain by parameterizing relations on configuration dimension. No downstream theorems are recorded yet, indicating this module serves as an entry point for semantic applications.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)