pith. sign in
module module high

IndisputableMonolith.Foundation.CostFirstExistence

show as:
view Lean formalization →

The CostFirstExistence module defines recognition existence by the vanishing of J-cost. It states that an object x exists precisely when J(x) equals zero and supplies immediate consequences such as cost positivity for non-existence. The module rests on the imported Cost and Constants modules to anchor the criterion in RS-native units.

claimAn element $x$ exists if and only if $J(x)=0$.

background

The module belongs to the Foundation domain and imports the J-cost function from the Cost module together with the base time quantum from Constants. The Constants module supplies the RS-native time quantum τ₀ = 1 tick. J-cost measures multiplicative deviation from unity under the Recognition Composition Law, and the module uses this to equate existence with zero cost.

proof idea

This is a definition module, no proofs. It introduces the predicate RSExists via the J-cost condition and records direct equivalences together with the positivity statement for non-existent objects.

why it matters in Recognition Science

The module supplies the existence criterion that supports the forcing chain (T0-T8) and later results on the phi-ladder. It implements the recognition existence step that precedes J-uniqueness and the derivation of spatial dimensions.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)