rs_true_or_of_left
plain-language theorem explainer
If a predicate P is RS-true under a cost bridge, dynamics B, seed c0 and target c*, then the disjunction of P with any Q is also RS-true. Researchers working on the operational ontology of Recognition Science cite this as the left half of the disjunction closure rule in Proposition 3.4. The proof is a direct term-mode unpacking of the RSTrue definition that preserves existence and target value while simplifying the stabilization condition along the orbit.
Claim. Let C be a configuration space, bridge a CostBridge mapping each element of C to a positive real, B a dynamics map on C, c0 a seed and c* a target configuration, and let P, Q be predicates from C to Bool. If c* is RS-existent, P holds at c*, and P stabilizes along the orbit of B from c0 to c*, then the predicate c ↦ P(c) ∨ Q(c) satisfies the same three conditions.
background
The module supplies the operational ontology of Recognition Science in which existence and truth arise as selection outcomes under cost minimization. CostBridge equips a configuration space C with a positive scalar map χ that feeds into defect calculations. RSTrue(P) holds when the target c* satisfies RSExists_cfg (zero defect), P(c*) is true, and the predicate stabilizes along the orbit of B from seed c0 to c* (the orbit eventually agrees with the value at c* on P). Upstream results supply the concrete bridge construction from the CPM2D model and the precise definition of RSTrue itself.
proof idea
The term proof introduces the three conjuncts of RSTrue for P (existence, value at c*, and stabilization). It then refines to the corresponding conjuncts for the disjunction by copying the first two and using the stabilization hypothesis together with simp to verify that the disjunction agrees with the target value along the orbit.
why it matters
This supplies the left case of the disjunction introduction rule (Proposition 3.4) and is used directly by the full rs_true_or_intro theorem that closes RSTrue under arbitrary disjunction. It thereby shows that RS-truth, defined via stability under recognition iteration, inherits the Boolean structure required by the selection rule without assuming classical logic as a primitive. The result sits inside the broader derivation of decidability and Boolean laws from the J-cost structure and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.