defect_zero_implies_exists
plain-language theorem explainer
Zero defect for positive real x implies x satisfies the existence predicate. Researchers formalizing the Law of Existence biconditional cite this direction to close the equivalence. The proof is a direct term construction that packages the two hypotheses into the Exists record.
Claim. If $x > 0$ and defect$(x) = 0$, then $x$ exists, where the existence predicate is the structure requiring both positivity and vanishing defect.
background
The module formalizes the Law of Existence as the equivalence $x$ exists iff defect$(x) = 0$. The defect functional equals the J-cost, so defect$(x) := J(x)$. The Exists predicate is the structure with fields pos : $0 < x$ and defect_zero : defect$(x) = 0$, matching the CostAxioms definition of existence as $0 < x$ and $J(x) = 0$.
proof idea
The proof is a one-line term that constructs the Exists record by supplying the positivity hypothesis to the pos field and the defect-zero hypothesis to the defect_zero field.
why it matters
This supplies the backward direction of the Law of Existence, supporting the biconditional law_of_existence and unity_unique_existent in the same module. It aligns with the framework claim that existence occurs precisely at cost minima, the golden-ratio fixed point. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.