$\nu_2(9^a-9^b)=3+\nu_2(a-b)$

Proved

Erdos195.nu2_nine_pow_sub

by Ethan Cheung Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmetic-progressionscombinatoricserdos-problems

For natural numbers $a\neq b$ ,

\nu_2\bigl(9^a-9^b\bigr)=3+\nu_2(a-b),

where $\nu_2$ is the $2$ -adic valuation on $\mathbb{Z}$ . This is the lifting-the-exponent lemma for $9=1+8$ . In the tree-witness approach to Erdős Problem 195 it says that two powers $3^e9^s$ , $3^e9^t$ of the same parity sit at level $3+\nu_2(t-s)$ of the binary residue tree. That fact is the basis of the bit-reversal words $W_{2^n}$ .

Formalization note: $\nu_2$ is padicValInt 2.

Preamble

import Mathlib
import Definitions.Def_Erdos195_tree

Formal statement

namespace Erdos195

theorem nu2_nine_pow_sub (a b : ℕ) (h : a ≠ b) :
    padicValInt 2 ((9 : ℤ) ^ a - 9 ^ b) = 3 + padicValInt 2 ((a : ℤ) - b) := by sorry

end Erdos195

Source

Erdős Problem 195 (https://www.erdosproblems.com/195); tree-witness framework; W_j construction designed by Grok Bot for Ethan Cheung (Oct 23 2026), proof outline by GPT, Lean-verified by Grok Bot

View graph

ν2(9a−9b)=3+ν2(a−b)\nu_2(9^a-9^b)=3+\nu_2(a-b)ν2​(9a−9b)=3+ν2​(a−b)

$\nu_2(9^a-9^b)=3+\nu_2(a-b)$