structured_set_singleton
plain-language theorem explainer
The theorem proves that the structured set of positive reals with vanishing defect coincides with the singleton containing unity. Researchers formalizing the Law of Existence would cite it to confirm that only unity satisfies the zero-defect condition. The proof applies set extensionality, simplifies the membership predicate, and splits cases using the defect-zero equivalence together with the explicit evaluation at one.
Claim. Let $S = { x > 0 : defect(x) = 0 }$. Then $S = {1}$.
background
The Law of Existence module formalizes the principle that an entity exists precisely when its defect vanishes. StructuredSet is defined as the collection of all positive reals x satisfying 0 < x and defect(x) = 0. The defect function is built from the J-cost J(x) = (x + x^{-1})/2 - 1, so zero defect marks exact unity.
proof idea
The proof proceeds by set extensionality. After simplification of the set-of predicate, the forward direction invokes defect_zero_iff_one to force x = 1. The reverse direction substitutes x = 1 and applies defect_at_one to recover the zero-defect membership.
why it matters
This pins the structured set to a singleton and thereby supports uniqueness of the existent. It directly precedes unity_unique_existent and law_of_existence in the module. Within Recognition Science it closes the base case of the forcing chain by exhibiting unity as the sole fixed point of J before the phi-ladder and higher-dimensional structures are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.