Lifting identity for binary digits of $c\cdot 9^t$

Proved

Erdos195.nine_pow_lift_bit

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

arithmetic-progressionscombinatoricserdos-problems

Let $c$ be an odd integer, $r,t\ge0$ , and $q=t\bmod 2^r$ . Write $\mathrm{bit}_k(x)=\lfloor x/2^k\rfloor\bmod2$ . Then

\mathrm{bit}_{r+3}\bigl(c\cdot9^t\bigr)\equiv \mathrm{bit}_{r+3}\bigl(c\cdot 9^{q}\bigr)+\mathrm{bit}_r(t)\pmod 2 .

So the binary digit of $c\cdot9^t$ at position $r+3$ is the digit for the reduced exponent $q$ , flipped exactly when bit $r$ of $t$ is $1$ . This follows from $9^{2^r}\equiv1+2^{r+3}\pmod{2^{r+4}}$ . In the tree-witness approach to Erdős Problem 195 it computes the bit forced at the node of a pair of same-parity powers of $3$ .

Formalization note: $\mathrm{bit}_k(x)$ is x / 2 ^ k % 2 (floor division on ℤ).

Preamble

import Mathlib
import Definitions.Def_Erdos195_tree

Formal statement

namespace Erdos195

theorem nine_pow_lift_bit (c : ℤ) (hc : Odd c) (r t : ℕ) :
    c * 9 ^ t / 2 ^ (r + 3) % 2 = (c * 9 ^ (t % 2 ^ r) / 2 ^ (r + 3) + (t / 2 ^ r : ℕ)) % 2 := 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

Lifting identity for binary digits of c⋅9tc\cdot 9^tc⋅9t

Lifting identity for binary digits of $c\cdot 9^t$