mem_structured_iff_exists
plain-language theorem explainer
The membership of a real in the structured set of zero-defect positives is equivalent to the existence predicate. Researchers formalizing the Law of Existence cite this when chaining equivalences to the complete statement that existence, zero defect, set membership, and equality to 1 are all the same. The proof is a term-mode biconditional that directly matches the two identical constructors for positivity and defect zero.
Claim. For any real number $x$, $x$ belongs to the set of positive reals with zero defect if and only if $x$ satisfies the existence predicate, where the set is defined as all $y > 0$ such that defect$(y) = 0$ and the predicate asserts both $0 < x$ and defect$(x) = 0$.
background
The Law of Existence module formalizes the claim that a positive real exists precisely when its defect vanishes. Defect is defined as defect$(x) := J(x)$, the cost function from the Recognition Science axioms. The structured set collects all positive reals at which this defect equals zero. The existence predicate is the structure whose two fields are positivity and defect zero, matching the CostAxioms formulation that a ratio exists iff $J(x) = 0$.
proof idea
The proof is a term-mode construction of the biconditional. It unpacks the membership pair (positivity and defect zero) directly into the existence structure for one direction and packs the existence fields back into the membership pair for the converse. No lemmas are applied; the two sides are definitionally identical.
why it matters
This equivalence is used inside the complete_law_of_existence theorem, which asserts that for $x > 0$ the statements Exists $x$, defect$(x) = 0$, membership in the structured set, and equality to 1 are all equivalent. It supplies the link between set-theoretic and predicate versions of the Law of Existence, supporting the claim that existence is economically inevitable because 1 is the unique defect minimizer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.