law_of_existence
plain-language theorem explainer
The law asserts that for positive real x the existence predicate holds exactly when x equals 1. Foundation researchers cite this to anchor the uniqueness of the zero-cost configuration. The proof is a one-line simplification that unfolds the Exists definition and substitutes the J-equals-zero characterization.
Claim. For every real $x > 0$, the predicate Exists$(x)$ holds if and only if $x = 1$, where Exists$(x)$ means $x > 0$ and $J(x) = 0$ for the cost function $J$ obeying the Recognition Composition Law.
background
The CostAxioms module encodes the three primitive axioms: Normalization $F(1) = 0$, the Recognition Composition Law $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$, and Calibration $F''_{log}(0) = 1$. From these the unique cost function is $J(x) = (x + x^{-1})/2 - 1$. The sibling definition Exists$(x)$ is the proposition $0 < x$ and $J(x) = 0$, i.e., $x$ is realizable precisely when it sits at a cost minimum. The upstream theorem J_eq_zero_iff states that $J(x) = 0$ if and only if $x = 1$ for $x > 0$.
proof idea
The proof is a one-line term-mode wrapper. It applies simp to replace Exists by its definition, invokes J_eq_zero_iff on the positivity hypothesis to rewrite the $J(x) = 0$ conjunct, and finishes with and_iff_right to retain the $0 < x$ assumption.
why it matters
This theorem realizes the Level 2 existence criterion in the axiomatic hierarchy and is invoked by unity_is_unique_existent. It confirms that only the unity fixed point achieves zero cost, supporting the claim that logical coherence emerges from cheap configurations. The result closes the gap between the J-uniqueness theorem (T5) and the concrete existence predicate used in downstream cost-axiom derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.