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

IndisputableMonolith.Modal.Possibility

show as:
view Lean formalization →

The Modal.Possibility module supplies the basic objects for modal reasoning in Recognition Science by defining a configuration as a point in recognition state space. It introduces a simplified Config type together with the J-cost function and its elementary properties to support possibility arguments. Researchers developing modal logic, actualization, or geometry in the framework cite this module as the common foundation. The module contains only definitions and direct lemmas with no tactic-heavy proofs.

claimA configuration $C$ is an element of the recognition state space, represented as a simplified LedgerState. The associated cost function satisfies $J(x) = (x + x^{-1})/2 - 1$ together with the elementary relations $J(x) = J(1/x)$, $J(x) = 0$ if and only if $x = 1$, and $J(x) > 0$ for $x > 0$, $x ≠ 1$.

background

The module imports the Law of Existence, whose central statement is that an object exists precisely when its defect vanishes. It therefore works in a setting where existence is reduced to a zero-defect condition before modal operators are introduced. Within this setting the module defines ConfigSpace as the ambient recognition state space and Config as its elements, using a deliberately simplified representation that stands in for the full LedgerState of the complete theory.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the core definitions that the parent Modal module, Actualization submodule, and ModalGeometry submodule all import. It therefore occupies the position of the entry point for any modal development that later invokes possibility, actualization, or geometric structure inside the Recognition framework.

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)