RSExists
plain-language theorem explainer
Recognition existence is formalized by declaring that RSExists(x) holds exactly when the J-cost of configuration x vanishes. Researchers working on pre-geometric selection principles cite this predicate as the anchor for the claim that only the unit configuration is stable under recognition dynamics. The declaration is a direct definitional abbreviation with no lemmas or tactics required.
Claim. The recognition existence predicate is defined by $RSExists(x) := J(x) = 0$ for $x : ℝ$, where $J$ is the J-cost function induced by the multiplicative recognizer.
background
The Cost-First Existence module encodes the pre-Big-Bang selection principle: stable patterns are those of minimum recognition cost. The J-cost function is the derived cost of a multiplicative recognizer's comparator and equivalently the cost assigned to recognition events. Upstream results establish that this cost is nonnegative and that the ontology version of RSExists augments vanishing cost with the positivity condition 0 < x.
proof idea
This is a direct definition: RSExists x is introduced by the equation Jcost x = 0. No lemmas are applied and no tactics are used; the declaration serves as the primitive predicate for equivalence and forcing results.
why it matters
The predicate supplies the core definition for CostFirstExistenceCert, which certifies equivalence to x = 1 and positive cost for all other positive reals. It is invoked in discreteness forcing theorems to show stable existence requires a discrete configuration space and in Godel dissolution results to identify the unique existent with unity. It implements J-uniqueness from the forcing chain and selects the self-similar fixed point as the origin of law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.