A proof of the Applegate-Lagarias Conjecture A and the 3x+1 growth exponent conjecture

For an integer \(a\) let \(\pi_a(x)\) be the number of integers \(n\) with \(|n|\le x\) whose trajectory under the \(3x+1\) map \(T\), given by \(T(n)=n/2\) for even \(n\) and \(T(n)=(3n+1)/2\) for odd \(n\), contains \(a\). In 1995 Applegate and Lagarias conjectured that for every \(a\) not divisible by \(3\) there is \(c_a>0\) with \(\pi_a(x)\ge c_a x\) for all \(x\ge |a|\) (Conjecture A). We prove this conjecture. For positive targets the input is a recently released theorem, formally verified in Lean: the predecessors of each positive target prime to \(3\) under the ordinary map \(n\mapsto n/2, 3n+1\) have positive lower density. Negative targets require new mathematics. Negation conjugates the \(3x+1\) dynamics on the negative integers to the \(3x-1\) dynamics on the positive integers, and we prove the corresponding density theorem for \(3x-1\). Its proof follows the architecture of the proof of that theorem. The sign change reverses one basic inequality, which costs a multiplicative factor at every generation of the inverse construction. We show that the product of these factors stays uniformly bounded. Ordinary and accelerated predecessor sets can differ only at targets \(a\equiv 4\pmod 6\), where \(T(2a)=a\) transfers the bound, and the target's membership in its own predecessor set gives the bound for every \(x\ge|a|\). As a corollary, \(\log\pi_a(x)/\log x\to1\), which proves the \(3x+1\) growth exponent conjecture. The complete argument, including the imported theorem, is formalized in Lean 4 with Mathlib and has been replayed independently by the Lean kernel.