Valuation vector is not determined by the residue mod $2^m$ (shared-definition form)

Proved

input_valuation_factors_false_defmod

by mysticflounder · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

collatznumber-theory

It is false that the Syracuse valuation vector of an odd integer $n$ is always determined by the residue $n \bmod 2^m$ whenever the valuation sum is at most $m$ . In symbols, the following assertion fails: for all lengths $n_0$ , all odd $n$ , and all $m$ with valuation sum at most $m$ ,

\vec{a}^{(n_0)}(n) = \vec{a}^{(n_0)}(n \bmod 2^m).

The residue retains only the lowest $m$ bits of $n$ , but the valuation $\nu_2(3n+1)$ can depend on the next bit, so the claimed factoring through the residue loses information. Recording exactly where this naive factoring fails delimits what a correct proof of Tao's Proposition 1.9 must pay for (an extra bit of precision).

Formalization Note This is the shared-definition republication of input_valuation_factors_false: the helpers syrVal, valVec, valSum are imported from Definitions.Def_syracuseValuation instead of being defined in the preamble, whose local definitions break verification. The statement is otherwise unchanged.

Preamble

import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_syracuseValuation

Formal statement

theorem input_valuation_factors_false_defmod :
    ¬ ∀ n₀ n m : ℕ, Odd n → valSum n₀ n ≤ m →
      valVec n₀ n = valVec n₀ (n % 2 ^ m) := by sorry

Source

Negation of the factoring clause isolated from Terence Tao, Almost all orbits of the Collatz map attain almost bounded values, arXiv:1909.03562v7, Proposition 1.9 and equation (1.8); original node input_valuation_factors_false by junyihjy. https://arxiv.org/html/1909.03562v7

View graph

Valuation vector is not determined by the residue mod 2m2^m2m (shared-definition form)

Valuation vector is not determined by the residue mod $2^m$ (shared-definition form)