Extremum obstruction: a least element traps safe words

Proved

Erdos195.extremum_obstruction

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

arithmetic-progressionscombinatoricserdos-problems

Let $R$ be a relation on $\mathbb{Z}$ satisfying $(\ast)$ , with a least element $z$ ( $z\mathrel{R}y$ for all $y\neq z$ ). Let $P$ be a safe list containing $z$ . Then no element $M$ appearing after $z$ in $P$ can be the maximum or the minimum of $P$ :

z\in P,\ \mathrm{Safe}_R(P),\ \mathrm{pos}_P(z)<\mathrm{pos}_P(M),\ M=\max P \text{ or } M=\min P \implies \bot.

This is the obstruction to running Ho's method on $\mathbb{Z}$ with a completion order that has a least element.

Formalization Note compLt R P x y holds when both lie in P with x at a smaller index, or x ∈ P and y ∉ P, or neither lies in P and R x y. Safe R P says there are no a and r ≠ 0 with compLt R P a (a+r), compLt R P (a+r) (a+2r) and compLt R P (a+2r) (a+3r).

P.idxOf is the index of the first occurrence in the list.

Preamble

import Mathlib
import Definitions.Def_Erdos195_defs

Formal statement

namespace Erdos195

theorem extremum_obstruction (R : ℤ → ℤ → Prop) (hB : Star R) (z : ℤ)
    (hz : ∀ y, y ≠ z → R z y) (P : List ℤ) (hS : Safe R P) (hzP : z ∈ P) (M : ℤ)
    (hMP : M ∈ P) (hzM : P.idxOf z < P.idxOf M)
    (hext : (∀ x ∈ P, x ≤ M) ∨ (∀ x ∈ P, M ≤ x)) : False := by sorry

end Erdos195

Source

New to this mission (obstruction to transferring B. S. Ho, arXiv:2609.12780, Lemma 2 to ℤ)

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