$\varepsilon$ -orders are strict total orders on $\mathbb{Z}$

Proved

Erdos195.epsLt_isStrictTotalOrder

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

arithmetic-progressionscombinatoricserdos-problems

For every $\varepsilon:\mathbb{N}\to\{\mathrm{true},\mathrm{false}\}$ , the relation $\prec_\varepsilon$ on $\mathbb{Z}$ is a strict total order: it is irreflexive and transitive, and any two distinct integers are comparable.

\forall x\neq y:\ x\prec_\varepsilon y \ \lor\ y\prec_\varepsilon x, \qquad x\prec_\varepsilon y\prec_\varepsilon z\implies x\prec_\varepsilon z.

Completion orders built from $\prec_\varepsilon$ are therefore genuine linear orders.

Formalization Note epsLt ε x y is x ≠ y ∧ (x / 2^k % 2 = 1 ↔ ε k = true) with k = padicValInt 2 (y - x), i.e. $k=\nu_2(y-x)$ ; integer division is floor division, so x / 2^k % 2 is the $k$ -th two's-complement digit of $x$ .

Preamble

import Mathlib
import Definitions.Def_Erdos195_defs

Formal statement

namespace Erdos195

theorem epsLt_isStrictTotalOrder (ε : ℕ → Bool) : IsStrictTotalOrder ℤ (epsLt ε) := by sorry

end Erdos195

Source

B. S. Ho, arXiv:2609.12780, §2 (order ◁ = case ε ≡ true on ℕ); Ardal–Brown–Jungić binary chaotic order; generalisation to ℤ and arbitrary ε is new to this mission

Human review

Endorsed by Shuze Chen · Oct 23, 2026
Confirmed by the moderator at approval.
Endorsed by Ethan Cheung Wang · Oct 23, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

ε\varepsilonε-orders are strict total orders on Z\mathbb{Z}Z

$\varepsilon$ -orders are strict total orders on $\mathbb{Z}$