rs_true_and
plain-language theorem explainer
rs_true_and establishes that a predicate formed by conjunction is RS-true exactly when each conjunct is RS-true, under a fixed cost bridge, dynamics B, seed c0 and target c_star. Researchers formalizing Boolean closure in the RS operational ontology cite it when building complex stable predicates from simpler ones. The proof unfolds RSTrue and Stabilizes then splits the iff into two directions, using case analysis on orbit values to transfer the common stabilization witness N to each conjunct separately.
Claim. Let bridge be a CostBridge on type $C$ (with positive real-valued map χ), let $B: C→C$ be the dynamics map, let $c_0,c_⋆∈C$, and let $P,Q:C→Bool$. Then $P∧Q$ is RS-true at $c_⋆$ under bridge, $B$, $c_0$ if and only if both $P$ and $Q$ are RS-true at $c_⋆$ under the same parameters. Here RS-true means: $c_⋆$ has zero defect via bridge, the predicate holds at $c_⋆$, and the predicate stabilizes along the orbit of $B$ from $c_0$ (i.e., eventually equals its value at $c_⋆$).
background
In the RS ontology predicates module, RSTrue is the operational definition of truth: for a predicate $P:C→Bool$, RSTrue(bridge, B, c0, c⋆, P) holds precisely when RSExists_cfg(bridge, c⋆) (zero defect under the bridge map χ), $P(c⋆)=true$, and Stabilizes(B, P, c0, c⋆). The Stabilizes predicate asserts existence of an $N$ such that for all $n≥N$, $P(B^{[n]}c_0)=P(c⋆)$. CostBridge supplies the scalar cost input χ with the positivity axiom ∀c, 0<χ(c). The module derives existence and truth from cost minimization under the unique J function rather than taking them as primitives.
proof idea
The tactic proof first unfolds RSTrue and Stabilizes. The forward direction extracts the shared existence witness and stabilization index N, then performs case analysis on the Boolean values of P and Q at c⋆ and along the orbit (via cases and simp_all) to produce separate witnesses for each conjunct. The reverse direction combines the two stabilization indices by taking their maximum and applies the individual orbit agreements to the conjunction via rw and simp.
why it matters
The result supplies the conjunction clause of the Boolean laws for RS-decidability inside the operational ontology. It directly supports the module's selection rule that truth equals stabilization under recognition iteration, thereby connecting to the broader forcing chain (T5 J-uniqueness through T8 D=3) and the Recognition Composition Law. No downstream uses are recorded yet, but the theorem closes a basic scaffolding step needed before complex predicates can be shown RS-real.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.