pith. sign in
module module moderate

IndisputableMonolith.Philosophy.MetaethicalPositionsFromConfigDim

show as:
view Lean formalization →

This module defines metaethical positions derived from configuration dimension in Recognition Science. Researchers linking RS foundations to ethics would cite the types and certificates it introduces. It consists entirely of definitions and count functions with no proofs.

claimThe module introduces the type $\text{MetaethicalPosition}$ together with the function $\text{metaethicalPosition_count}$ and the certificate $\text{MetaethicalPositionsCert}$ obtained from configuration dimension.

background

The module sits in the philosophy domain and imports only the RS time quantum $\tau_0 = 1$ tick from IndisputableMonolith.Constants. It supplies the sibling declarations MetaethicalPosition, metaethicalPosition_count, MetaethicalPositionsCert and metaethicalPositionsCert that encode positions derived from configuration dimension.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the definitional layer for metaethical positions in the Recognition Science framework. No downstream theorems are recorded, so it functions as a self-contained philosophical interface.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)