RSDecidable
plain-language theorem explainer
RSDecidable packages the two background conditions required for Boolean reasoning over RSTrue predicates in the Recognition Science ontology. It asserts that the target configuration exists under the cost bridge and that the predicate stabilizes along the given dynamics from the seed point. Researchers formalizing negation and disjunction laws for truth in RS cite this definition when stating hypotheses. The definition is a direct conjunction of the two component predicates RSExists_cfg and Stabilizes.
Claim. A predicate $P : C → Bool$ is RS-decidable at $(c_*, B, c_0)$ relative to a cost bridge if $c_*$ exists under the bridge (its cost image has zero defect) and $P$ stabilizes along the orbit of $B$ from $c_0$ to $c_*$.
background
The RS ontology module treats existence and truth as outcomes of cost minimization under the unique J function rather than primitives. CostBridge is the structure supplying a positive real-valued map χ from configurations in C to costs. RSExists_cfg declares that a configuration exists precisely when its bridged cost equals 1. Stabilizes asserts that after some finite number of iterations of the dynamics B the predicate P agrees with its value at the target for all further steps.
proof idea
The definition is a one-line conjunction of RSExists_cfg bridge c_star and Stabilizes B P c0 c_star. No tactics or lemmas are applied beyond the direct packaging of the two upstream predicates.
why it matters
RSDecidable supplies the hypothesis for the Boolean laws on RSTrue, directly feeding rs_true_neg_iff_neg_rs_true and rs_true_or_iff. It operationalizes the selection rule stated in the module doc-comment, converting the Meta-Principle into a cost theorem. The definition sits inside the T0-T8 forcing chain by ensuring stabilization conditions hold before classical logic is recovered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.