rs_true_or_intro
plain-language theorem explainer
rs_true_or_intro shows that RSTrue is closed under disjunction introduction: if RSTrue(P) or RSTrue(Q) holds under a CostBridge and dynamics B, then RSTrue(P or Q) follows. Researchers building the logical structure of stable predicates in Recognition Science cite it as the or-introduction rule. The proof is a direct case split that applies the left and right introduction lemmas.
Claim. If RSTrue(bridge, B, c₀, c*, P) or RSTrue(bridge, B, c₀, c*, Q), then RSTrue(bridge, B, c₀, c*, λc. P(c) ∨ Q(c)), where RSTrue requires that c* is RS-existent under the bridge, the predicate holds at c*, and the predicate stabilizes along the orbit of B from c₀.
background
A CostBridge maps configurations of type C to positive real costs via an observable χ. RSTrue(bridge, B, c₀, c*, P) holds precisely when RSExists_cfg(bridge, c*) is true, P evaluates to true at c*, and Stabilizes(B, P, c₀, c*) holds. The module treats existence and truth as derived selection outcomes under J-cost minimization rather than primitive notions, with the Meta-Principle recovered as a cost theorem.
proof idea
The term-mode proof uses rintro to split the input disjunction into cases, then applies rs_true_or_of_left to the left case and rs_true_or_of_right to the right case. Each of those lemmas unpacks the RSTrue triple (existence, value, stabilization) and re-verifies the conditions for the disjoined predicate.
why it matters
This is Proposition 3.4 and supplies the introduction direction for disjunction in the RS predicate logic. It is invoked by rs_true_or_iff (Theorem 3.5) to obtain the biconditional under RS-decidability of both predicates. The result contributes to the Boolean closure properties of stable predicates within the operational ontology derived from the J-function and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.