Exact Exponent Cylinders, Precision Budgets, and Singular Coding in Accelerated Syracuse Dynamics

Version 6 of the Collatz/accelerated Syracuse research program. This mathematical note follows the published v5 methodology retrospective. It develops finite arithmetic and Lean 4 results, identifies concrete limits of several proposed global arguments, and corrects a statement about 2-adic continuity in v4. It does not prove the Collatz conjecture. Formalized results. For every nonempty finite word of positive Syracuse exponents, the Lean theorem syracuseWordMatches_iff_exactResidue characterizes an exact match by the affine congruence (3^L n + C) mod 2^(A+1) = 2^A, where L is the word length and A its exponent sum. A companion theorem treats repeated blocks. Other Lean declarations establish an exact 2-adic precision loss along a matched expansive word, a compatible-label switching identity, a short-trace lasso obstructing a proposed three-counter rank, necessary cycle and finite-barrier conditions, and positive odd inputs arbitrarily close to the singular 2-adic point whose accelerated outputs remain distinct. The supplementary archive contains the pinned Lean package source and a finite diagnostic for affine switching defects. Scope of the deductions. Uniqueness and natural density of the finite exponent cylinder, the 2-adic coding discussion, and an explicit cancellation family are argued in the paper; they are not presented as newly formalized Lean theorems. The one-residue-class observation was stated earlier by Ross, so this record claims no priority for it. The defect diagnostic checks finite cases and is not a global certificate. The paper states the remaining universal descent and nontrivial-cycle obligations explicitly. Correction to v4. The v4 discussion treated the totalized accelerated map on all 2-adic integers as continuous and used that assertion in a global conjugacy argument. The finite arithmetic witness in v6 shows that the totalized map is discontinuous at -1/3. Infinite positive-exponent coding is therefore stated on its appropriate invariant odd domain, and no global continuity or conjugacy claim is used. Research context. The note distinguishes these pointwise finite identities from the almost-all results of Tao and Inselmann. It also compares contemporary formalization and coding work in the bibliography. None of those results is used as a premise for a universal Collatz conclusion. Files and verification. The PDF is the complete v6 paper. The supplementary ZIP includes its LaTeX source, a self-contained Lean source snapshot with Lean/Mathlib pins, the new diagnostic and literature audit, and a checksum manifest. The frozen PDFs of published v1–v5 are not part of this v6 ZIP. The paper separates Lean-checked claims from paper-level arguments and proposed research targets. The pinned toolchain is Lean 4.29.1; the paper records the need for a separate replay on a newer Lean release. Version relation. This record is intended as a new version of the same Zenodo concept record, 10.5281/zenodo.20021537. Previous published version: v5, 10.5281/zenodo.20554750. Project source: PieroBorgatta/Collatz.