Collatz Map Basics

This is a collection of autoformalizations of definitions and elementary lemmas associated with the Collatz Conjecture. The focus is first on facts needed to build up recent arguments by Rozier and Terracol [ 5 ] . Secondly, we attempt to be more complete regarding elementary lemmas to allow shorter proofs of more advanced theorems. The work is motivated by an urge to understand current research better, but also by the idea of a specialized library of autoformalizations, should the need arise for it.