This paper is the companion to “Diophantine Confinement and the Syracuse Reduc-tion” 11, providing the full computational evidence, extended proofs, and connectionsto related problems.We prove that if the transverse walk associated to a Collatz trajectory has eventuallylinear drift, then the trajectory is eventually bounded and periodic. The key tool isa geometric series bound on the correction ratio r(t) = C(t)/2ν2 (t) , which satisfies aCollatz-like recurrence driven by the trajectory’s parity sequence. Cycle elimination isproved for all cycles with ∆3 ≤ 79 odd steps per period. The argument is formalizedin approximately 9 040 lines of Lean 4 across 36 files with eight external axioms, allciting published theorems, and six explicit sorry declarations, each equivalent to theCollatz conjecture.Extensive computational evidence supports the framework: a 100-billion branchlocus computation (25.1 × 1012 Collatz steps) reveals cell saturation at 21,632 cells, aDiophantine ghost island controlled by Baker-type bounds, and the equilibrium cusp atp∗ = 1/(1 + log2 3). Application to the 5x + 1 and 7x + 1 maps reveals an inverted beltstructure and a phase transition at q = 4, with autocorrelation diagnostics that measureDiophantine approximation quality. Connections to Furstenberg’s ×2, ×3 conjectureare developed via a spectral gap theorem and entropy bridge analysis. A connectionto Littlewood’s conjecture o
Janik John (Sat,) studied this question.