rs_true_or_iff
plain-language theorem explainer
Under RS-decidability of predicates P and Q with respect to a cost bridge and orbit map B, RSTrue of the disjunction holds exactly when RSTrue of P or RSTrue of Q holds. Researchers deriving Boolean properties inside the Recognition Science ontology would cite this equivalence (Paper Theorem 3.5). The proof constructs the biconditional by case analysis on the Boolean values at the stable point c_star for the forward direction and direct application of the introduction lemma for the reverse.
Claim. Let $C$ be a type, let $bridge$ be a CostBridge supplying a positive cost map on $C$, let $B : C → C$ be a dynamics, and let $c_0, c_⋆ ∈ C$. Let $P, Q : C → Bool$ be predicates that are both RS-decidable, i.e., $c_⋆$ exists under the bridge and each predicate stabilizes along the orbit of $B$ from $c_0$ to $c_⋆$. Then $RSTrue(bridge, B, c_0, c_⋆, P ∨ Q)$ holds if and only if $RSTrue(bridge, B, c_0, c_⋆, P)$ or $RSTrue(bridge, B, c_0, c_⋆, Q)$ holds.
background
The module defines an operational ontology in which truth is not primitive but arises as stabilization under recognition iteration driven by the J-cost. A CostBridge is a structure supplying a positive scalar map χ : C → ℝ that embeds configurations relative to a reference. RSTrue(bridge, B, c₀, c⋆, P) holds precisely when c⋆ exists under the bridge (zero defect), P evaluates to true at c⋆, and P stabilizes along the orbit of B from seed c₀. RSDecidable packages the existence and stabilization hypotheses required for classical Boolean manipulation of such predicates.
proof idea
The term proof opens with constructor to split the biconditional. The forward direction performs case analysis on P c⋆ and then on Q c⋆; the case where both are false contradicts the assumption that the disjunction holds at c⋆ via simp, while the remaining cases assemble the corresponding RSTrue witness from the shared existence datum and the relevant stabilization component of hdecP or hdecQ. The reverse direction applies the auxiliary lemma rs_true_or_intro directly.
why it matters
This result (Paper Theorem 3.5) supplies disjunction distributivity for the RSTrue predicate, allowing classical Boolean algebra to be performed inside the cost-minimization ontology. It directly supports the module's selection rule that a predicate is true precisely when it stabilizes under recognition iteration. The theorem belongs to the Boolean-laws fragment that follows the core definitions of RSExists and RSTrue; downstream work on logical combinations of stable properties relies on it. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.