RSTrue_classical
plain-language theorem explainer
RSTrue_classical embeds any proposition P directly as an RS truth predicate without dynamical context or cost structure. Researchers reducing ontology statements to classical Boolean reasoning cite it when the full RSTrue with bridges and stabilization is unnecessary. The definition is a one-line abbreviation that equates the predicate to its input proposition.
Claim. For any proposition $P$, the classical recognition truth predicate satisfies $RSTrue_{classical}(P) := P$.
background
The RS ontology treats truth as a selection outcome: a predicate P is RS-true when it stabilizes under recognition iteration without drift. The full RSTrue predicate, defined in the same module, requires a CostBridge, dynamics B, seed c0 and stable c_star, plus a configuration predicate, and holds precisely when RSExists_cfg holds at c_star, P evaluates true there, and Stabilizes applies along the orbit. RSTrue_classical strips away all of this structure for pure propositions, serving as the classical placeholder noted in the module documentation on operational ontology.
proof idea
The declaration is a direct abbreviation that sets RSTrue_classical P to P with no lemmas or tactics applied.
why it matters
RSTrue_classical supplies the classical limit case that feeds the equivalence rs_true_classical_iff, confirming identity with ordinary truth. It supports Boolean reasoning inside the RS framework while the full ontology derives existence and truth from J-cost minimization and defect collapse to zero, as described in the module's connection to the meta-principle. The definition closes the placeholder gap between classical logic and the cost-based selection rule without invoking the phi-ladder or eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.