Exists
plain-language theorem explainer
The Exists structure packages the predicate that a real number x exists in the Recognition Science framework exactly when x is positive and defect(x) vanishes. Researchers formalizing cost minima or the Law of Existence would cite this predicate when stating equivalences to x = 1. The declaration is a direct structure definition with two fields and no proof steps.
Claim. A real number $x$ satisfies the existence predicate if $0 < x$ and the defect of $x$ equals zero.
background
In this module the defect functional is defined by defect x := J x for x > 0, where J is the cost function imported from CostAxioms. The module supplies a literal formalization of the Law of Existence: x exists if and only if defect(x) = 0. Upstream CostAxioms.Exists is the J-based version 0 < x ∧ J x = 0, which this structure mirrors by substituting the defect abbreviation.
proof idea
This is a structure definition that directly encodes the two conditions positivity and zero defect. No lemmas or tactics are invoked; the declaration simply packages the predicate for use in later equivalences.
why it matters
The definition feeds the complete_law_of_existence theorem and the law_of_existence equivalence in CostAxioms, both of which conclude that existence holds precisely at x = 1. It supplies the predicate required by the Recognition framework's central claim that defect collapse occurs only at the golden-ratio fixed point. The structure closes the interface between the J-cost formulation and the defect-based statements used throughout the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.