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

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
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
preprint

Natural-number and arctic matrix interpretations alone make no progress, in any dimension, on the Collatz rewriting system

Hiroyuki Nashida
Zenodo (CERN European Organization for Nuclear Research)
Logic, programming, and type systems
preprint

Natural-number and arctic matrix interpretations alone make no progress, in any dimension, on the Collatz rewriting system

Hiroyuki Nashida
preprint en

Abstract

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.

Zenodo (CERN European Organization for Nuclear Research)
Logic, programming, and type systems
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

Natural-number and arctic matrix interpretations alone make no progress, in any dimension, on the Collatz rewriting system — Hiroyuki Nashida · Zenodo (CERN European Organization for Nuclear Research) (2026) | TGRS Research Map | TGRS