rs_true_neg_iff_neg_rs_true
plain-language theorem explainer
Under RS-decidability a predicate P is RS-true at the stable point c_star if and only if its negation is not RS-true. Researchers formalizing the operational ontology of Recognition Science cite this result to close the Boolean algebra on stable predicates. The proof is a direct term construction that invokes the one-way implication rs_true_neg_imp_neg_rs_true and then builds the converse by case analysis on the Boolean value of P at c_star together with the stabilization hypothesis.
Claim. Let $C$ be a type, let bridge be a CostBridge on $C$, let $B:C→C$, let $c_0,c_*∈C$, and let $P:C→Bool$. If $P$ is RS-decidable (i.e., $c_*$ is RS-existent and $P$ stabilizes along the orbit of $B$ from $c_0$ to $c_*$), then $P$ is RS-true at $c_*$ if and only if the predicate $c↦¬P(c)$ is not RS-true at $c_*$.
background
The module OntologyPredicates supplies the operational definitions of existence and truth in Recognition Science. RSExists_cfg bridge c_star asserts that the configuration c_star has zero defect under the cost map χ supplied by the CostBridge structure. Stabilizes B P c0 c_star asserts that the Boolean value of P eventually agrees with its value at c_star along the orbit generated by B. RSTrue bridge B c0 c_star P is the conjunction of these three conditions: zero defect at c_star, P(c_star)=true, and stabilization. RSDecidable is the conjunction of RSExists_cfg and Stabilizes, the minimal background that permits classical Boolean reasoning inside the RS setting.
proof idea
The proof proceeds by constructor to split the biconditional. The forward direction is discharged by exact application of the upstream lemma rs_true_neg_imp_neg_rs_true. For the converse, assume ¬RSTrue P, unpack the decidability hypothesis into existence and stabilization, then perform by_cases on P c_star. The true case yields an immediate contradiction with the negation assumption. The false case supplies the required witnesses for RSTrue of the negated predicate by rewriting the stabilization orbit with the false value.
why it matters
This theorem completes the negation law for RSTrue once RS-decidability is assumed, thereby embedding classical Boolean negation inside the Recognition Science ontology. It sits inside the sequence of Boolean closure results that follow the definitions of RSExists and RSTrue in the module. The result is a direct consequence of the cost-minimization selection rule stated in the module documentation and supports any later argument that treats RS-true predicates as a Boolean algebra under the J-cost dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.