Natural-number and arctic matrix interpretations alone make no progress, in any dimension, on the Collatz rewriting system
Preprint. Yolcu, Aaronson and Heule encoded the Collatz map as an 11-rule rewriting system, collatz-T of the Termination Problem Database, and suggested proving that no matrix or arctic interpretation establishes its termination. We show that natural-number matrix interpretations in the form of Endrullis, Waldmann and Zantema, and arctic interpretations, applied on their own, make no progress on it in any dimension. A natural-number matrix interpretation of collatz-T with all top-left entries at least 1 that weakly orients all 11 rules strictly orients none of them, and so does an arctic interpretation over the natural numbers with finite top-left entries, for collatz-T and also for the system of the modulo-8 conjecture; hence rule removal with these interpretations alone removes no rule at any stage. The same holds for the reversed systems and, for collatz-T, for the matrix interpretations of Hofbauer and Waldmann that compare corner entries. Without the condition on the top-left entries, natural-number interpretations in the form of Endrullis, Waldmann and Zantema remove no rule in the top forms of Yolcu, Aaronson and Heule, and natural-number and arctic reduction pairs remove no pair of the essential component of the dependency pair problem. In dimension at most 2, the results for rule removal in the form of Endrullis, Waldmann and Zantema follow from earlier work of Valbuena. The main theorems are kernel-checked in Lean 4, using only the three standard axioms; the results on transformations are computer-assisted. The general core form of matrix interpretations, lexicographic comparisons, other semirings, and proof pipelines in which other techniques act first are not covered. None of the results settles the Collatz conjecture. Lean code, computations and verification logs are on GitHub. Prepared with substantial assistance from generative AI (Anthropic Claude); see the disclosure in the paper. Not yet reviewed by human experts.
Authors
- Hiroyuki Nashida
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-10-08
- DOI
- https://doi.org/10.5281/zenodo.23147025
- Primary Topic
- Logic, programming, and type systems
- Type
- preprint