pith. sign in
module module high

IndisputableMonolith.Foundation.CostFirstExistence

show as:
view Lean formalization →

The CostFirstExistence module encodes the base claim that an object x exists precisely when its J-cost is zero. Researchers building the cost-first ontology or the forcing chain would cite it to ground existence before deriving phi or dimensions. The module collects the equivalence and its immediate corollaries via imports from Cost and Constants.

claim$x$ exists if and only if $J(x)=0$, where $J(x)=cosh(log x)-1$.

background

The module sits in the Foundation domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the cost function from the Cost module. The supplied doc-comment states the central claim directly: recognition existence holds exactly when J(x) vanishes. Sibling declarations such as RSExists and costFirstExistenceCert formalize the predicate and its certification.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the existence predicate that precedes J-uniqueness (T5) and the subsequent forcing steps to phi, the eight-tick octave, and D=3. It fills the cost-first proposition that underpins the entire Recognition framework. No downstream theorems are listed in the used_by edges.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)