rs_true_or_of_right
plain-language theorem explainer
If RSTrue holds for predicate Q under CostBridge, dynamics B, seed c0 and target c_star, then RSTrue also holds for the disjunction of Q with any predicate P. Researchers establishing Boolean closure properties of stable predicates in Recognition Science cite this as the right half of disjunction introduction. The proof unpacks the three conjuncts of RSTrue for Q and transfers them to the disjunction via Boolean simplification.
Claim. Let RSTrue(Q) mean that c_star is RS-existent under the bridge (defect vanishes), Q(c_star) holds, and Q stabilizes along the orbit of B from c0 to c_star. Then RSTrue(Q) implies RSTrue(P ∨ Q) for any predicate P.
background
The OntologyPredicates module defines an operational ontology in which existence and truth arise from cost minimization. CostBridge maps each configuration C to a positive real scalar via an observable χ, supplying the input to defect calculations. RSTrue bridge B c0 c_star P is the conjunction of three conditions: RSExists_cfg bridge c_star, P c_star = true, and Stabilizes B P c0 c_star (the predicate eventually agrees with its value at c_star along the orbit).
proof idea
The term proof introduces the RSTrue hypothesis as the triple ⟨hex, hval, N, hN⟩. It refines the goal to the corresponding triple for the disjunction, using simp on hval to obtain the truth value at c_star and simp on hN n hn together with hval to obtain the stabilization witness.
why it matters
This supplies the right case of Proposition 3.4 on Boolean laws for RS predicates and is invoked by the full disjunction introduction theorem rs_true_or_intro. It contributes to the infrastructure showing that RS-truth is closed under disjunction, consistent with stabilization under the J-cost function and the Recognition Composition Law. No open scaffolding questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.