pith. sign in
module module high

IndisputableMonolith.Modal.Possibility

show as:
view Lean formalization →

Modal.Possibility supplies the configuration space and J-cost function as primitives for modal logic development in Recognition Science. It defines Config as points in recognition state space using a simplified LedgerState representation. The module is imported by Modal, Actualization, and ModalGeometry. Content consists of type definitions and elementary J lemmas with no complex proofs.

claimLet Config be the type of configurations, each a point in recognition state space. Let $J :$ Config $→ ℝ$ satisfy $J(x) ≥ 0$, with $J(x) = 0$ precisely when $x$ is the identity configuration, and related transition properties.

background

The module sits in the modal domain and provides simplified objects for modal logic development. Its doc-comment states that a configuration is a point in recognition state space, serving as a stand-in for the full LedgerState. It imports LawOfExistence, whose doc-comment gives the sharp formalization that x exists if and only if defect(x) = 0. Sibling definitions include ConfigSpace, identity_config, and the family of J lemmas (J_nonneg, J_at_one, J_zero_iff_one, J_transition, J_stasis).

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the parent Modal module and its submodules Actualization and ModalGeometry, supplying the state-space primitives required for modal constructions. It sets up the objects needed to apply the Recognition Composition Law and the T5–T8 forcing chain steps within modal contexts. Downstream modules rely on these definitions to develop possibility and geometry.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (36)