Decreasing diagrams are complete for confluence

Your AI and this story

Key facts

• Paper: ‘Decreasing Diagrams are Complete for Confluence’, arXiv 2610.06368 [cs.LO], 5 Oct 2026; Jörg Endrullis (Vrije Universiteit Amsterdam), Ievgen Ivanov (Taras Shevchenko National University of Kyiv), Femke van Raamsdonk (Vrije Universiteit Amsterdam)
• Confluence: a nondeterministic computation ‘always yields the same result, regardless of the order in which steps are taken’. Van Oostrom’s decreasing diagrams technique reduces it to a local condition: ‘a system is confluent whenever its transitions admit a locally decreasing labeling. Essentially all classical confluence criteria arise as corollaries.’
• Question (1993, RTA Problem 56): ‘Does every confluent transition system admit a locally decreasing labeling?’ Known before: yes for countable systems, ‘and recently up to the first uncountable cardinal ℵ_1’
• Result: ‘every confluent transition system admits a locally decreasing labeling using only three labels. This bound is optimal, as two labels do not suffice even at the first uncountable cardinality.’
• Paper: ‘This outcome was not foregone: van Oostrom conjectured that decreasing diagrams are incomplete … and related questions about uncountable directed sets are independent of ZFC.’
• Paper: ‘To the best of our knowledge, these are the first unconditional completeness results for methods of proving confluence.’
• Verification: ‘the entire development is independently machine-checked in two proof assistants, Isabelle/HOL and Lean; both formalizations are archived on Zenodo’. The Isabelle proof shows the result holds in ZFC; the paper notes that ‘a Lean proof alone would not give this’
• AI disclosure: ‘the formalizations were developed with the assistance of Anthropic’s Claude, under the authors’ direction and review. The authors take full responsibility for the correctness and presentation of this work.’ No Claude model is named