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

IndisputableMonolith.Modal.Possibility

show as:
view Lean formalization →

The Modal.Possibility module defines configurations as points in recognition state space together with the J-cost function and its immediate properties. It supplies the simplified objects needed to develop modal logic before full LedgerState integration. The module is imported by the parent Modal module and by Actualization and ModalGeometry. Definitions rest on the upstream Law of Existence and prepare the ground for possibility and actualization statements.

claimLet Config be a type whose elements are points in recognition state space. ConfigSpace is the corresponding space. The map $J :$ Config $→ ℝ$ satisfies $J ≥ 0$, $J(1) = 0$, $J(x) = 0$ iff $x = 1$, and the transition identity $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$.

background

Recognition Science begins from the Law of Existence, which the upstream LawOfExistence module states as: an entity x exists if and only if defect(x) = 0. The present module replaces the full LedgerState with a simplified Config type that stands for a point in recognition state space. It introduces ConfigSpace, the identity configuration, and the J function together with its non-negativity, zero-at-one, positivity-off-one, and transition lemmas.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the basic objects required by the Modal, Actualization, and ModalGeometry modules. It therefore anchors the modal layer of the framework, linking the Law of Existence directly to the state space on which possibility statements are later defined.

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)