We revisit the decidability of livelock detection in self-disabling unidirectional ring protocols, a problem shown to be undecidable in general by Klinkhamer and Ebnenasir via reduction from the periodic domino problem. Despite this, practical protocols routinely admit finite proofs of livelock freedom via the same tiling constraints, and synthesis of parameterized self-stabilizing rings has been shown to be decidable -- suggesting a gap between theory and practice. We identify the source of this gap: the apparent unboundedness of livelock reasoning is an artifact of working in the transition space. By lifting to an \emph{equivariant product space} -- the space of transition-witness pairs coupled by the zigzag equivariance conditions of Farahat -- we show that self-disabling induces a structure in which closure and period are preserved under backward propagation. This yields a bounded witness property: every livelock, constructed from a set of local transitions $T$, admits a representative as a local cycle of length at most $|T|^2$ in a finite product graph, independent of the ring size. We derive a sound and complete decision procedure via greatest fixed-point iteration on the product graph. Our results demonstrate that decidability emerges not by restricting the problem syntactically, but by exposing its underlying finite combinatorial structure. We validate on over 4,300 protocols with zero errors, extend to $(1,1)$-asymmetric protocols, and derive a circulation law classifying livelocks by ring size. Code and algebraic foundation are at the URL https://github.com/cosmoparadox/mathematical-tools.

翻译：我们重新审视自禁用单向环协议中活锁检测的可判定性问题。Klinkhamer与Ebnenasir通过周期多米诺问题的归约证明该问题在一般情况下不可判定。然而实际协议常通过相同拼图约束提供活锁自由的有限证明，且参数化自稳定环的综合已被证明可判定——这表明理论与实际之间存在鸿沟。我们识别出此鸿沟的根源：活锁推理的表面无界性是转换空间工作的假象。通过提升至_等变乘积空间_——即由Farahat锯齿等变条件耦合的转换-见证对空间——我们证明自禁用特性会诱导一种结构，其中闭包性与周期性在反向传播下得以保持。由此得出有界见证性质：由局部转换集T构造的每个活锁，在有限乘积图中存在长度至多|T|^2的局部环作为其代表，且此界与环规模无关。我们通过乘积图上的最大不动点迭代推导出可靠且完备的决策过程。研究结果表明可判定性的涌现并非源于对问题的语法限制，而是通过揭示其底层有限组合结构。我们基于零错误率的4,300余个协议完成验证，扩展至(1,1)-非对称协议，并推导出按环规模分类活锁的循环定律。相关代码与代数基础见https://github.com/cosmoparadox/mathematical-tools。