rsExists_iff_one
plain-language theorem explainer
Recognition existence for positive real x holds exactly when x equals 1, the unique point where J-cost vanishes. Pre-Big-Bang selection arguments cite this biconditional to ground existence in cost minimization. The proof unfolds the definition of RSExists and splits the biconditional, deriving a contradiction from positivity of J-cost away from one and substituting the zero value at one.
Claim. For every real $x > 0$, the predicate RSExists$(x)$ (defined by $J(x) = 0$) holds if and only if $x = 1$.
background
The module formalizes the cost-first selection principle: a pattern $x > 0$ exists in the recognition sense precisely when its J-cost is zero, so that laws emerge as the unique J-minimizing configurations. RSExists is defined by RSExists$(x) :=$ Jcost $x = 0$. This rests on the upstream lemmas Jcost_pos_of_ne_one (Jcost $x > 0$ whenever $x > 0$ and $x ≠ 1$) and Jcost_unit0 (Jcost $1 = 0$).
proof idea
The proof unfolds RSExists to the equation Jcost $x = 0$, then applies constructor to obtain both directions of the biconditional. The forward direction assumes the equation and reaches a contradiction with $x ≠ 1$ via Jcost_pos_of_ne_one. The reverse direction substitutes $x = 1$ and invokes Jcost_unit0.
why it matters
This equivalence supplies the central claim packaged inside costFirstExistenceCert, realizing the module statement that RSExists$(x) ↔ J(x) = 0 ↔ x = 1$. It anchors the pre-geometric cost landscape in which physics is selected by J-minimization rather than posited by axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.