existence_zero_cost
plain-language theorem explainer
The theorem establishes that the J-cost vanishes at the unit element. Recognition Science researchers would cite it to formalize existence as the unique zero-cost configuration. The proof is a direct term application of the unit lemma for the J-cost function.
Claim. $J(1) = 0$, where the cost function is given by $J(x) = (x-1)^2 / (2x)$.
background
The module Existence from J-Cost develops the pre-Big-Bang identification of existence with the zero-cost state in Recognition Science. The central definitions are the J-cost function, expressed as the squared ratio $J(x) = (x-1)^2 / (2x)$, together with the five modes of existence whose dimension is fixed at D = 5. The local setting states that J(1) = 0 marks the unique cost-zero configuration while J(x) > 0 for x ≠ 1 and J(x) → ∞ as x → 0.
proof idea
The proof is a one-line term wrapper that applies the Jcost_unit0 lemma. That lemma itself reduces by simplification on the definition of Jcost.
why it matters
The result supplies the existence_zero field inside the ExistenceCert definition, which aggregates the five modes. It directly realizes the RS claim that existence equals the cost-zero condition and sits downstream of the J-uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.