Odd $u$ , odd target $t$ : $(0,u,t)$ is $\varepsilon$ -safe when $\varepsilon_0=1$ and $\varepsilon$ differs from $u$ at digit $\nu_2(t-u)$

Proved

Erdos195.odd_two_letter_odd_target

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

arithmetic-progressionscombinatoricserdos-problems

Fix $\varepsilon:\mathbb{N}\to\{0,1\}$ and the $2$ -adic total order on $\mathbb{Z}$ given by $x\prec_\varepsilon y$ iff $x\neq y$ and the $k$ -th two's-complement digit of $x$ equals $\varepsilon_k$ , where $k=\nu_2(y-x)$ . A finite word $Q$ of integers is $\varepsilon$ -safe if the sequence "the letters of $Q$ in order, then all remaining integers in $\prec_\varepsilon$ -order" contains no monotone $4$ -term arithmetic progression. Write $u_k$ for the $k$ -th binary digit of $u$ . Let $u$ and $t$ be odd integers with $t\neq u$ , and put $k=\nu_2(t-u)$ . If $\varepsilon_0=1$ and $\varepsilon_k\neq u_k$ , then

(0,\,u,\,t)\ \text{is } \varepsilon\text{-safe}.

So for an odd second letter $u$ , every odd target can be appended to $(0,u)$ directly, after fixing a single digit of $\varepsilon$ (a step in Ho-style constructions of $4$ -AP-free permutations of $\mathbb{Z}$ , Erdős Problem 195).

Formalization note: Safe, epsLt, bitOne are from Definitions.Def_Erdos195_defs; $\varepsilon_k\ne u_k$ is written ¬ (bitOne u k ↔ ε k = true).

Preamble

import Mathlib
import Definitions.Def_Erdos195_defs

Formal statement

namespace Erdos195

theorem odd_two_letter_odd_target (ε : ℕ → Bool) (u t : ℤ) (hu : u % 2 = 1) (ht : t % 2 = 1)
    (htu : t ≠ u) (h0 : ε 0 = true)
    (hk : ¬ (bitOne u (padicValInt 2 (t - u)) ↔ ε (padicValInt 2 (t - u)) = true)) :
    Safe (epsLt ε) [0, u, t] := by sorry

end Erdos195

Source

Erdős Problem 195 (https://www.erdosproblems.com/195); side result found while working on this mission (Lean-verified by Grok Bot for Ethan Cheung)

View graph

Odd uuu, odd target ttt: (0,u,t)(0,u,t)(0,u,t) is ε\varepsilonε-safe when ε0=1\varepsilon_0=1ε0​=1 and ε\varepsilonε differs from uuu at digit ν2(t−u)\nu_2(t-u)ν2​(t−u)

Odd $u$ , odd target $t$ : $(0,u,t)$ is $\varepsilon$ -safe when $\varepsilon_0=1$ and $\varepsilon$ differs from $u$ at digit $\nu_2(t-u)$