This paper presents KO7, a minimal operator-only term rewriting system with seven constructors and eight reduction rules, designed to investigate self-verifying computation. No external axioms, imported logic, or pre-existing arithmetic are used. Standard termination methods fail on this system. We document ten proof strategies that collapse at the same barrier: duplication of the step argument in the recursor. The rec-succ rule redistributes its argument into both the function application and the recursive call, defeating every additive measure. This failure is not a defect but a necessary feature of any system capable of sequential computation. To resolve this, we define SafeStep, a guarded fragment restricted by a delta-phase bit. For this fragment, a novel triple-lexicographic measure (combining phase bits, Dershowitz-Manna multiset ordering, and ordinal ranking) succeeds, supporting a mechanically verified normalizer with proven totality and soundness. We state a fundamental conjecture: No relational operator-only TRS can have its full-system termination proved by internally definable methods. A relational TRS is one capable of internalized sequential computation, a property shared by Turing machines, lambda calculus, and recursive functions. All such systems require a recursor that inherently creates the duplication barrier. This reveals Pre-Arithmetic Incompleteness. Unlike Goedel's theorems, which require arithmetic sufficient for encoding, this barrier appears at a more primitive layer: in operator systems possessing only order and recursion, before arithmetic emerges. The complete Lean 4 formalization (around 7,000 LOC) is available at https://github.com/MosesRahnama/OperatorKO7.

翻译：本文提出KO7——一个仅含算子的最小项重写系统，包含七个构造子和八条归约规则，旨在研究自验证计算。该系统不使用外部公理、导入逻辑或预设算术。标准终止性证明方法在此系统上均告失效。我们记录了十种在相同障碍处崩溃的证明策略：递归子中步进参数的重复。rec-succ规则将其参数同时分配到函数应用和递归调用中，这击败了所有加法性度量。该失效并非缺陷，而是任何具备顺序计算能力的系统必需的特性。为解决此问题，我们定义了SafeStep——一个通过δ相位位约束的受保护片段。针对该片段，一种新颖的三重字典序度量（结合相位位、Dershowitz-Manna多重集序和序数分级）取得成功，支持构建经机械验证的规范化器，并证明了其完全性与可靠性。我们提出一个基本猜想：任何纯关系型算子TRS的完全系统终止性都无法通过内部可定义的方法证明。关系型TRS指能够实现内化顺序计算的系统，该特性为图灵机、λ演算和递归函数所共有。所有此类系统都需要一个本质上会产生重复障碍的递归子。这揭示了前算术不完全性。与哥德尔定理需要足以编码的算术系统不同，此障碍出现在更原始的层面：在仅拥有序和递归的算子系统中，于算术显现之前即已存在。完整的Lean 4形式化（约7000行代码）可在https://github.com/MosesRahnama/OperatorKO7获取。