Stabilizes
plain-language theorem explainer
The Stabilizes definition captures when a predicate P on configurations eventually agrees with its value at a target c_star along the forward orbit of a map B from seed c0. Researchers formalizing RS-truth and decidability in the ontology predicates cite it to replace informal notions of stability with an explicit tail condition on iterates. The definition is introduced directly via existential quantification over a natural number N that bounds the agreement for all larger n.
Claim. A predicate $P : C → Bool$ stabilizes under the iteration of a map $B : C → C$ from initial configuration $c_0$ to target $c_*$ when there exists $N ∈ ℕ$ such that for all $n ≥ N$, $P(B^n(c_0)) = P(c_*)$.
background
The module supplies the operational ontology of Recognition Science in which existence and truth arise as selection outcomes under the J-cost functional rather than as primitives. Configurations belong to a type C equipped with a CostBridge that evaluates defect via the upstream defect definition (equal to J on positive reals). The module documentation states the selection rule: P is true iff P stabilizes under recognition iteration. Upstream results supply the defect functional from LawOfExistence and the Configuration structure from InitialCondition as positive-ratio ledgers.
proof idea
The declaration is a direct definition that encodes eventual constancy of P on the orbit tail. No lemmas or tactics are invoked; the body is the primitive existential statement over N that is later unfolded inside the definitions of RSTrue and RSDecidable.
why it matters
Stabilizes supplies the dynamical stability clause required by RSTrue and RSDecidable in the same module, which in turn support the Boolean laws such as rs_true_and. It also appears in GodelDissolution to contrast stabilization (defect zero) with divergence. The definition thereby realizes the module's claim that truth is verifiable via cost minimization and recognition iteration, connecting to the meta-principle derived from defect collapse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.