We present a minimal operator-only term rewriting system with seven constructors and eight reduction rules. Our main contribution is a mechanically-verified proof of strong normalization for a guarded fragment using a novel triple-lexicographic measure combining a phase bit, multiset ordering (Dershowitz-Manna), and ordinal ranking. From strong normalization, we derive a certified normalizer with proven totality and soundness. Assuming local confluence (verified through critical pair analysis), Newman's Lemma yields confluence and therefore unique normal forms for the safe fragment. We establish impossibility results showing that simpler measures, such as additive counters, polynomial interpretations, and single-bit flags, provably fail for rules with term duplication. The work demonstrates fundamental limitations in termination proving for self-referential systems. We state a conjecture: no relational operator-only TRS can have its full-system termination proved by internally definable methods. Here "relational" is equivalent to "capable of ordered computation" - systems with a recursor enabling iteration over successors, comparison, or sequential counting. Such recursors necessarily redistribute step arguments across recursive calls, defeating all additive termination measures. This structural limitation applies to any TRS expressive enough to encode ordered data. All theorems have been formally verified in a proof assistant. The formal development is available to program committee members and referees upon request for purposes of peer review.

翻译：我们提出一个仅含运算符的最小项重写系统，包含七个构造子和八条归约规则。主要贡献是通过一种结合相位位、多重集序（Dershowitz-Manna）和序数排名的三重字典序度量，对受保护片段给出了机械验证的强正规化证明。基于强正规化性质，我们推导出一个经认证的正规化器，其完全性与可靠性均已得证。在满足局部合流性（通过临界对分析验证）的前提下，依据纽曼引理可推出合流性，从而确保安全片段存在唯一正规形式。我们建立了不可能性结果，证明对于含项复制规则的系统，简单度量方法（如加法计数器、多项式解释和单比特标志）必然失效。这项工作揭示了自指系统终止性证明的根本局限。我们提出一个猜想：任何纯关系运算符TRS的完整系统终止性均无法通过内部可定义方法证明。此处“关系型”等价于“具备有序计算能力”——即系统需包含能在后继运算、比较或顺序计数上迭代的递归子。此类递归子必然在递归调用间重新分配步进参数，从而破坏所有加法型终止度量。该结构局限性适用于任何能编码有序数据的TRS。所有定理均在证明助手中完成形式化验证，形式化开发资料可供程序委员会成员及审稿人在同行评审过程中按需获取。