Pith. sign in
module module high

IndisputableMonolith.Foundation.CostFirstExistence

show as:
view Lean formalization →

The CostFirstExistence module defines recognition existence of an object x precisely when its J-cost vanishes. It would be cited by any derivation that reduces physical existence claims to the zero set of the recognition cost functional. The module is assembled from imported definitions in Cost and Constants with no additional proof obligations.

claimAn object \(x\) is recognized to exist if and only if \(J(x)=0\), where \(J\) is the recognition cost.

background

The module resides in the Foundation domain and imports the RS time quantum (\tau_0=1) tick from Constants together with the cost machinery from the Cost module. Its DOC_COMMENT states that recognition existence of (x) holds precisely when (J(x)) equals zero. This implements the cost-first ontology for all subsequent constructions in Recognition Science.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the RSExists predicate that underpins the forcing chain from T0 to T8, in particular enabling J-uniqueness at T5 and the Recognition Composition Law. It provides the base case for existence arguments throughout the framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)