complete_law_of_existence
plain-language theorem explainer
For positive real x the existence predicate is equivalent to vanishing defect, membership in the structured set, and equality to unity. Researchers formalizing the Recognition Science axioms cite this to establish that only the unit value is realizable. The proof is a term-mode biconditional constructed by applying the unity characterization and membership lemmas in each direction.
Claim. For $x > 0$, the predicate Exists$(x)$ holds if and only if defect$(x) = 0$, $x$ belongs to the structured set, and $x = 1$.
background
The Law of Existence module supplies a literal formalization of the statement that x exists precisely when its defect vanishes. Defect is the J-cost functional on positive reals; the upstream CostAxioms.Exists definition states that x exists iff 0 < x and J(x) = 0, identifying existence with a cost minimum. The local Exists structure packages the two conditions 0 < x and defect x = 0, while StructuredSet is defined as the collection of all positive reals whose defect is zero.
proof idea
The term proof opens the biconditional with constructor. In the forward direction it extracts defect zero from the Exists hypothesis, applies mem_structured_iff_exists.mpr to obtain structured-set membership, and invokes exists_iff_unity.mp to recover x = 1. In the reverse direction it substitutes the supplied equality x = 1 and closes with defect_at_one together with the positivity of one.
why it matters
The declaration unifies the four listed characterizations inside the Law of Existence module, confirming that the zero-defect condition forces x = 1. It sits downstream of exists_iff_unity and mem_structured_iff_exists and thereby closes the equivalence chain begun by the CostAxioms.Exists definition. Within the Recognition framework it sharpens the statement that existence coincides with the J-cost minimum at the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.