Termination by Novelty: A Machine-Checked Theory of Anti-Regress Guards for Reflective Governance Processes — Why Step-Local Change Guards Cannot Stop Regress, and What Can

Abstract

Reflective processes — governance loops, self-review cycles, self-evolving software pipelines — face a canonical failure mode: infinite regress, the accumulation of meta-deliberation without state update. The MOBIUS anti-regress architecture (the "M guard") answers this operationally: continuation is justified only if the successor state is admissible and the transition is semantically non-zero, with explicit no-change fixation as a first-class terminal. Prior work stated this as a control form and validated its mechanical enforcement empirically. This paper supplies the missing mathematical layer. We formalize guarded reflective transition systems and prove four results.【proved】(i) The step-local guard — "each step changes something" — is insufficient in principle: a two-state oscillator satisfies it forever (Proposition 1). (ii) The history-global novelty guard terminates: if the semantic state space has finite capacity N at the working resolution (finite packing number), every guarded run performs at most N − 1 steps before the only admissible continuation is explicit fixation (Theorem 1); the bound is tight. (iii) Termination also follows from any well-founded progress measure, yielding an explicit step bound for checkpoint/rollback governance cycles (Theorem 2, Corollary 2.1). (iv) Guard violation is logically equivalent to the existence of a recurrence pair — two semantically indistinguishable states at different times — which identifies exactly what an ideal loop detector must measure (Theorem 3). We further prove that windowed detectors leak: for every window length w there is a guard-satisfying infinite run of period w + 1 (Proposition 5), establishing a theoretical floor for bounded-memory loop detection and a concrete design consequence for deployed detectors. Proposition 1 and the two termination theorems are machine-checked in Lean 4 (core, no external libraries; the checked artifact accompanies the paper; the tightness of the Theorem 1 bound is by an elementary hand proof). We close with an exploratory consistency check against a production self-evolution ledger (seven generations, live detector scores) and a falsification section. Theory paper T1 of the MOBIUS 2026-08 theory series (six papers, T1–T6). Version 0.1, deposited as a preprint; journal submission of a revised version is planned, and the journal version may differ. AI co-observer: Claude Fable 5 (Anthropic), working method only; the registered author is the human author alone.