exists_implies_defect_zero
plain-language theorem explainer
If a positive real x satisfies the existence predicate in Recognition Science, then its defect vanishes. Researchers formalizing the Law of Existence cite this to establish the forward direction of the x-exists-iff-defect-zero equivalence. The proof is a direct one-line projection of the defect_zero field from the Exists hypothesis structure.
Claim. Let $x$ be a positive real. If $x$ exists (i.e., $0 < x$ and defect$(x) = 0$), then defect$(x) = 0$.
background
The Law of Existence module formalizes the biconditional that a ratio x exists precisely when its defect vanishes. The Exists predicate is a structure with two fields: positivity (0 < x) and defect_zero (defect x = 0). The defect functional is defined locally as defect x := J x, where J is the cost function from upstream CostAxioms. Upstream CostAxioms.Exists states: def Exists (x : ℝ) : Prop := 0 < x ∧ J x = 0, with the accompanying note that existence corresponds to being at a cost minimum, the only minimum occurring at x = 1.
proof idea
This is a one-line term proof that applies the defect_zero field of the Exists hypothesis h.
why it matters
The theorem supplies the forward implication of the Law of Existence equivalence stated in the module doc-comment. It supports the full biconditional law_of_existence (Exists x ⟺ DefectCollapse x) and the uniqueness result unity_unique_existent. In the Recognition framework it aligns with the cost minimum at the golden-ratio fixed point where J(x) = 0, consistent with the T5 J-uniqueness and T6 phi fixed-point landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.