RSTrue
plain-language theorem explainer
RSTrue defines a predicate P as RS-true at configuration c_star under dynamics B from seed c0 precisely when the cost bridge maps c_star to a zero-defect value, P holds at c_star, and P remains constant along the forward orbit of B. Logicians and physicists working on Recognition Science ontology cite this when replacing primitive truth with a stabilization outcome derived from J-cost minimization. The definition is a direct three-clause conjunction with no additional lemmas.
Claim. Let $C$ be a type of configurations and let $bridge$ be a cost bridge supplying a positive real map $χ : C → ℝ$. A predicate $P : C → Bool$ is RS-true at $c_*$ under the dynamics $B : C → C$ from seed $c_0$ when $RSExists(χ(c_*))$ holds, $P(c_*) = true$, and there exists $N ∈ ℕ$ such that $P(B^{[n]}(c_0)) = P(c_*)$ for all $n ≥ N$.
background
The module establishes an operational ontology in which existence and truth arise as selection outcomes under the unique J-cost function rather than as primitives. RSExists_cfg states that a configuration c exists exactly when its image under the cost bridge has zero defect. Stabilizes requires that the boolean value of P eventually agrees with its value at c_star along the orbit of B. The module doc states: 'P is true ⟺ P stabilizes under recognition iteration' and 'existence and truth are not primitive notions - they are selection outcomes determined by cost minimization under the unique J function'. Upstream, CostBridge supplies the observable map χ with positivity, while the GodelDissolution module supplies the orbit-convergence notion of stabilization.
proof idea
This is a definition that directly expands to the conjunction RSExists_cfg bridge c_star ∧ P c_star = true ∧ Stabilizes B P c₀ c_star. No tactics or lemmas are invoked; the body is the explicit conjunction of the three operational conditions.
why it matters
RSTrue supplies the truth predicate used in downstream results such as ontology_summary (which assembles the coherent stack RSExists, RSTrue, RSReal) and godel_not_obstruction (which shows Gödel incompleteness does not obstruct RS closure). It operationalizes the Meta-Principle by making truth a derived stabilization property under J-cost dynamics, replacing the placeholder def RSTrue (P : Prop) : Prop := P. The declaration sits in the foundation layer that feeds the eight-tick octave and D = 3 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.