PRH | Aux | 4.3.5 • A Sceptic Introduction to the Proof of the Collatz Conjecture

A Sceptic Introduction to the Proof of the Collatz Conjecture For Readers Who Arrive Ready to Refute Aleksandar Perišić October 2025 If you came here to poke holes, you’re in the right place. This note is the fast, human-facing on-ramp: minimal formulas, maximal clarity, and a concrete checklist for what would actually break the proof. Where the authors are coming from (skepticism included) First, rest assured: the authors share your skepticism—amplified by having to audit every seam. We did not set out to “prove Collatz.” We carried a method (the blur viewpoint) through a few other problems and then—hesitantly—pointed it at Collatz, knowing several outcomes were possible: 1. Fail: blurring could not be turned back into sharp, certifiable inequalities (a hint Collatz might be false or at least resistant to this lens). 2. Semi-win: a Lyapunov-type certificate exists in principle, but with no usable bound on its size. 3. Pyrrhic win: a certificate exists but lives at an astronomically large modulus (“Googlenumber scale”)—correct but useless. 4. Least likely: a concrete, small certificate materializes. We fully expected (3). In that mindset, anything small would be dismissed—just as checking the first billions of numbers doesn’t prove Collatz. Yet the data kept saying the same thing: a closed certificate at modulus 213. We tried to break it. Repeatedly. The one idea that looks trivial only after the fact Two non-obvious moves turned out to be decisive: 1. Work on a finite residue graph. Reduce to the odd residues modulo 2 k , with one outgoing edge per class. No infinite graphs, no heroic combinatorics. Just a finite functional digraph. 2. Acknowledge a small, honest blur budget.Mixing +and × is like switching lenses (time/frequency). There’s an unavoidable “toll.” Track it as a small nonnegative number ρ . Without it, the key inequality refuses to close. Once you do these two things, the rest is standard max-plus folklore: cycle means nonpositive ⇐⇒ there exists a potential ϕ⇐⇒ Bellman–Ford relaxation stabilizes, all on the finite residue graph. That potential then yields a one-line drift inequality for the actual integers, by algebraic telescoping. No algorithm ever touches an infinite graph. 1 “But why 2k? Couldn’t you pick another modulus?” You could, but 2 k is canonical here. The valuation v2 (3 n + 1) becomes residue-determined off a single exceptional class, giving a clean, tiny table of edge weights and one conservative edge. Other moduli mostly create more exceptions and a larger finite check without changing the story. What we thought we were seeing (and what stayed when we stripped it down) We kept tightening the analysis. Paradoxically, the more carefully we bounded every term, the smaller the observed slack became until it matched the tight bar forced by the unique mod-8 edge. In hindsight this is exactly what should happen: precision removes wishful slack. At the end of the trimming, what remained was the most boring thing in the world: a finite table, a set of linear (max-plus) inequalities, and the word PASS. Okay, what would actually falsify the proof? Here is the short, surgical list. Any one of these breaks it: 1. A directed residue cycle with strictly positive average weight (contradicts feasibility). 2. A single violated residue inequality in the certificate table. 3. A bad interval bound (e.g. for log 2, log 3, or a tiny geometric tail) used in the verification. 4. An algebraic slip in deriving the drift inequality from the residue inequalities. Items (1)–(2) are finite and fully machine-checkable. Items (3)–(4) are local and easy to isolate. Why Isabelle/HOL? Because the certificate is finite and the bounds are rational intervals, we could formalize the check. We ported the essentials to Isabelle/HOL and asked it, in effect: “Please find a violation.” It did not. We also regenerated the 2 13 table via independent code paths (C#; a separate system); every line agreed; we surrounded each value with a certified interval. This wasn’t about theatrics; it was about eliminating the last “this feels too clean” doubt. Why it took so long (and why it still feels weird) Collatz has a cultural gravity: it’s discrete, so many expect a purely discrete proof. But addition and multiplication pull you into different lenses (time vs. frequency); the uncertainty principle between them is real in everyday algebra, and ignoring it just hides the toll. The “blur” isn’t a fashion choice; it is the book-keeping needed to cross that lens boundary honestly. Once you pay the toll, the max-plus certificate falls into the most classical of finite frameworks. What this is (and isn’t) • Is: a finite, verifiable Lyapunov certificate on the residue graph, yielding a monotone drift for the integer dynamics and an explicit, small modulus 213. • Isn’t: a plea to accept continuous methods on faith. The blur is condensed to a number ρ . Everything that matters happens in a finite table and inequalities you can read and check. 2 How to engage as a skeptic (quick path) 1. Open the artifact (certificate CSV) and the verifier. 2. Check the interval bounds (they are spelled out; tails are finite geometric estimates). 3. Run the Bellman–Ford style relaxation on the finite residue graph and confirm stabilization. 4. Inspect the worst-slack edge; compare to the tight mod-8 bound. 5. If you like, simulate random odd trajectories; watch the drift decrease after the small threshold. If any of this fails, you have a real bug. If all of it passes, you’ve reproduced the proof. Where to go next (and why we published a lot) We deliberately put everything on Zenodo: a compact proof, an Isabelle/HOL check, a studentfriendly worksheet with ∼ 30 tasks, a plain-language essay on the blur idea, and code to rebuild the certificate. Not to overwhelm; to remove ambiguity and lower the barrier for independent verification. We will also release a short video walking through the finite residue graph and the drift picture—no barrage of equations, just the moving parts. Final thought. If you still feel that “something this simple can’t be right,” try flipping the question: once you admit a tiny, honest toll for switching lenses, what, precisely, forbids a finite max–plus certificate from existing at some modulus? In our case it appears at 2 13 . That is the whole mechanism. Why this note exists (and a gentle warning). Collatz attracts attention not just because it is concise, but because it sits on a seam between addition and multiplication—two operations we often treat as if they shared a single “native” lens. They do not. The blur budget is not a stylistic flourish; it is a small, explicit price for crossing that seam. We are not claiming exclusivity of approach, nor asking anyone to like this one on aesthetic grounds. We are saying: if one insists a priori on a purely discrete path and dismisses any argument that makes the lens-switch toll visible, one may keep missing the same structural point indefinitely. Whether or not this proof is to your taste, please do not let taste be the reason to ignore the deeper message: problems that mix +and × reliably surface an “uncertainty” between lenses. Accounting for it—even in a minimal, finite way—can turn an allegedly intangible phenomenon into a checkable certificate. Our hope is that, even for readers who remain unconvinced by this route, the note nudges attention toward that seam, where many other hard problems seem to live. Acknowledgements and reproducibility All verification artifacts (tables, bounds, source, and formal scripts) are archived with DOIs and include command-line instructions to reproduce a PASS. The formal component in Isabelle/HOL (lemmas, certificates, and checks) is kept as close to the prose notation as the proof assistant allows. Bibliography • Perišić, A. (2025). Soft-Addition and Soft-Multiplication and the Channel–Switch Error. Zenodo. doi:10.5281/zenodo.17218980. 3 • Perišić, A. (2025). Collatz Without the Mystique of Addition and Multiplication. Zenodo. doi:10.5281/zenodo.17220058. •Perišić, A. (2025). Collatz Proof Verification: Isabelle/HOL. Zenodo. doi:10.5281/zenodo.17308278. 4