Prove2Me

Erdős #195: tree-witness 22-adic orders on Z\mathbb{Z}

Definition
Erdos195_tree

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

arithmetic-progressionscombinatoricserdos-problems

A tree witness is a function θ(k,r)∈{0,1}\theta(k,r)\in\{0,1\} defined on the nodes (k,r)(k,r), k≥0k\ge0, 0≤r<2k0\le r<2^k, of the infinite binary tree of residues modulo powers of 22. For distinct integers x,yx,y let k=ν2(y−x)k=\nu_2(y-x), the lowest binary position where the two's-complement expansions of xx and yy differ, so that x≡y(mod2k)x\equiv y\pmod{2^k}. Define

x≺θy  ⟺  x≠y and bitk(x)=θ(k, x mod 2k).x\prec_\theta y\iff x\neq y\ \text{and}\ \mathrm{bit}_k(x)=\theta\bigl(k,\ x \bmod 2^k\bigr).

Thus at each node of the binary tree, θ\theta chooses which child subtree comes first. The ε\varepsilon-orders ≺ε\prec_\varepsilon of Def_Erdos195_defs are the special case θ(k,r)=εk\theta(k,r)=\varepsilon_k, independent of rr. These orders are used as tail orders for Ho-style constructions of 44-AP-free permutations of Z\mathbb{Z} (Erdős Problem 195).

Formalization note: θ : ℕ → ℤ → Bool; only the values at 0 ≤ r < 2^k matter, since the second argument is always x % 2^k.

Definition code
import Mathlib
import Definitions.Def_Erdos195_defs

/-!
# Erdős Problem 195 — tree-witness orders on ℤ

A tree witness `θ : ℕ → ℤ → Bool` assigns a preferred bit `θ k r` to each node `(k, r)` of the
binary tree of residues (`r` is used modulo `2^k`; only `0 ≤ r < 2^k` matters).
For `x ≠ y` with `k = ν₂(y - x)`, `x ≺_θ y` iff the `k`-th two's-complement digit of `x` is `1`
exactly when `θ k (x mod 2^k) = true`. The ε-orders `epsLt ε` are the case `θ k _ = ε k`.
-/

namespace Erdos195

/-- The tree-witness order on ℤ. -/
def treeLt (θ : ℕ → ℤ → Bool) (x y : ℤ) : Prop :=
  x ≠ y ∧ (bitOne x (padicValInt 2 (y - x)) ↔
    θ (padicValInt 2 (y - x)) (x % 2 ^ padicValInt 2 (y - x)) = true)

end Erdos195
Source
Erdős Problem 195 (https://www.erdosproblems.com/195); tree-witness orders suggested by GPT 6 Astra, formalized by Grok Bot for Ethan Cheung

View graph