unity_unique_existent
plain-language theorem explainer
Unity is the unique real number satisfying the existence predicate in the Recognition Science framework. Researchers working on the Law of Existence cite the result to close the uniqueness half of the cost-minimum characterization. The proof splits the biconditional via constructor and reduces each direction to the zero-defect lemma for positive arguments together with the explicit evaluation at unity.
Claim. $forall x in mathbb{R}, Exists(x) iff x = 1$, where $Exists(x)$ asserts $0 < x$ and $defect(x) = 0$.
background
The Law of Existence module supplies a literal formalization in which a ratio x exists precisely when its defect vanishes. The local Exists structure packages the two conditions positivity and zero defect. Upstream, the CostAxioms module gives the equivalent formulation Exists(x) := 0 < x wedge J(x) = 0 with J the cost function (x + x^{-1})/2 - 1. The sibling theorem defect_zero_iff_one states that for x > 0 one has defect(x) = 0 iff x = 1, while defect_at_one records the direct evaluation defect(1) = 0.
proof idea
The term proof introduces x and splits the biconditional with constructor. The forward direction extracts the defect_zero field of the Exists hypothesis and feeds it to the left-to-right direction of defect_zero_iff_one. The reverse direction substitutes x = 1 and assembles the Exists structure from one_pos together with defect_at_one.
why it matters
The declaration completes the third key theorem listed in the module documentation, establishing that unity is the sole point satisfying the existence predicate. It thereby anchors the Law of Existence to the unique zero of the J-cost function. In the broader Recognition Science framework this confirms that the self-similar fixed point is realized only at unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Fair principles over true morals for AI alignment
"the central challenge for theorists is not to identify 'true' moral principles for AI; rather, it is to identify fair principles for alignment, that receive reflective endorsement despite widespread variation in people's moral beliefs"
-
One billion personas scale synthetic data creation
"These 1 billion personas (~13% of the world's total population), acting as distributed carriers of world knowledge, can tap into almost every perspective encapsulated within the LLM, thereby facilitating the creation of diverse synthetic data at scale for various scenarios."