IndisputableMonolith.Philosophy.ExistenceFromJCost
The module formalizes the identification of physical existence with the vanishing of the J-cost in Recognition Science. Researchers tracing the ontology of the framework from the Cost module onward would cite it when grounding existence claims in the zero-cost condition. The module is built from a short sequence of definitions and one-line lemmas that classify existence modes by their J values.
claimExistence holds precisely when the J-cost vanishes: $J=0$.
background
The module imports IndisputableMonolith.Cost, which supplies the J-cost function $J(x)=(x+x^{-1})/2-1$ together with the Recognition Composition Law. It introduces ExistenceMode as an inductive type whose constructors label distinct cost regimes, with existence_zero_cost establishing that the distinguished zero-cost constructor satisfies $J=0$. The surrounding philosophy section places this identification inside the T0-T8 forcing chain, where J-uniqueness (T5) already forces the self-similar fixed point phi.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the direct link between existence and J=0 that later results on the phi-ladder and mass formulas presuppose. It therefore sits immediately downstream of the Cost module and upstream of any theorem that invokes existenceCert or existenceModeCount. The doc-comment states the core claim in one line: Existence = J = 0.
scope and limits
- Does not derive the explicit algebraic form of J from more primitive axioms.
- Does not treat dynamical evolution or time-dependent costs.
- Does not connect the zero-cost condition to specific particle spectra or coupling constants.
- Does not address whether non-zero J modes can be realized in a completed theory.