exists_implies_defect_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the converse that zero defect implies existence.
- Does not identify explicit values of x that satisfy the predicate.
- Does not extend to negative reals or non-real numbers.
- Does not derive physical constants or dimensional constraints.
formal statement (Lean)
72theorem exists_implies_defect_zero {x : ℝ} (h : Exists x) : defect x = 0 :=
proof body
Term-mode proof.
73 h.defect_zero
74
75/-- **Law of Existence (Backward)**: Zero defect (with x > 0) implies existence. -/