exists_iff_unity
plain-language theorem explainer
A positive real x satisfies the existence predicate in Recognition Science precisely when x equals 1. Researchers formalizing the Law of Existence cite this to equate the defect-minimizing condition with unity. The proof is a term-mode construction that applies the defect-zero characterization in both directions of the biconditional.
Claim. For $x > 0$, $Exists(x) ↔ x = 1$, where $Exists(x)$ means $x > 0$ and $defect(x) = 0$.
background
The module formalizes the Law of Existence as the statement that x exists if and only if defect(x) = 0. The Exists structure requires two fields: positivity (0 < x) and defect_zero (defect x = 0). Upstream CostAxioms defines an equivalent Exists as 0 < x ∧ J x = 0, while defect_zero_iff_one proves defect x = 0 ↔ x = 1 for x > 0, with defect built from the J-cost J(x) = (x + x^{-1})/2 - 1.
proof idea
The proof is a term-mode wrapper. It builds the forward direction by projecting the defect_zero field from the Exists structure and applying defect_zero_iff_one.mp; the reverse direction pairs the positivity hypothesis with defect_zero_iff_one.mpr.
why it matters
This result is invoked by complete_law_of_existence to obtain the full chain of equivalences that includes membership in StructuredSet. It supplies the direct characterization step in the Law of Existence module, connecting to J-uniqueness (T5) and the phi fixed point (T6) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.