A common Syracuse exponent prefix forces one residue class
Provedsyracuse_valuation_prefix_residuecollatzmodular-arithmeticnumber-theory
Consider two finite natural-number chains satisfying the Syracuse affine step identities with the same first k exponents. Let S be the sum of those exponents and suppose S is below an integer threshold n'. If each final value satisfies divisibility of 3N+1 by 2^(n'-S), then the two initial values are congruent modulo 2^n'. This is an algebraic consequence of the stated identities and divisibility conditions; it does not assume the exponents are exact valuations and does not assert a probabilistic tail bound.
Preamble
import Mathlib
Formal statement
theorem syracuse_valuation_prefix_residue (k n' : ℕ) (a N₁ N₂ : ℕ → ℕ) (h₁ : ∀ i, i < k → 2 ^ a i * N₁ (i + 1) = 3 * N₁ i + 1) (h₂ : ∀ i, i < k → 2 ^ a i * N₂ (i + 1) = 3 * N₂ i + 1) (hS : (∑ i ∈ Finset.range k, a i) < n') (hfinal₁ : 2 ^ (n' - ∑ i ∈ Finset.range k, a i) ∣ 3 * N₁ k + 1) (hfinal₂ : 2 ^ (n' - ∑ i ∈ Finset.range k, a i) ∣ 3 * N₂ k + 1) : Nat.ModEq (2 ^ n') (N₁ 0) (N₂ 0) := by sorry
Source
Deterministic residue-class forcing argument in Terence Tao, Almost all orbits of the Collatz map attain almost bounded values, arXiv:1909.03562v7, Section 4, proof of Lemma 4.1, following the displayed congruence modulo 2^{n'}. https://arxiv.org/html/1909.03562v7 . This formalization abstracts the two chains and sufficient divisibility hypotheses; it is not the full probabilistic Lemma 4.1.