cafeinst/CollatzConjecture: Isabelle formalization of Collatz information barriers

**Important: This version has been superseded.** A substantially revised Isabelle/HOL formalization is available ascafeinst/CollatzConjecture: Isabelle formalization of Collatz information barriers | Zenodo.Readers interested in the current formalization should consult version 6.0. The goal of this theory is to formalize an information-theoretic barrier for a broad and natural class of trace-based proof strategies for the Collatz 3n+1 conjecture. It proves a conditional result: under explicit assumptions about how computational trace information is represented and preserved, no finite proof certificate can establish global convergence for all inputs.