RSExists_cfg
plain-language theorem explainer
RSExists_cfg lifts the real-valued existence predicate to arbitrary configuration spaces C equipped with a CostBridge. It declares that c exists precisely when the bridged scalar χ(c) has vanishing J-cost. Workers on the operational ontology of Recognition Science cite this to treat existence as a derived cost-minimization outcome. The definition is a direct one-line wrapper applying the upstream RSExists to the bridge image.
Claim. Let $C$ be a type and let $χ : C → ℝ$ be the cost map of a bridge with $χ(c) > 0$ for all $c$. Then $c$ satisfies configuration-level RS existence precisely when $J(χ(c)) = 0$.
background
The OntologyPredicates module treats existence and truth as selection outcomes under the unique J-cost function rather than primitives. A CostBridge on $C$ supplies a map $χ : C → ℝ$ together with the positivity axiom $∀ c, 0 < χ c$. The upstream RSExists predicate on the reals is defined by RSExists $x$ := Jcost $x$ = 0 and holds uniquely at $x$ = 1.
proof idea
The declaration is a one-line wrapper that applies the upstream RSExists predicate to the scalar value bridge.χ c.
why it matters
RSExists_cfg supplies the existence component required by the downstream definitions of RSTrue and RSDecidable. Those combine existence of $c_star$ (via this definition), truth of $P$ at $c_star$, and stabilization along the orbit. In the Recognition framework this realizes the selection rule that $x$ exists iff defect($x$) → 0 under coercive projection, replacing assumed existence with a cost-derived notion and connecting to the Meta-Principle derived from the cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.