Safe prefixes of a -AP-free enumeration are exactly the -closed cuts
ProvedErdos195.prefix_safe_iff_closed_cutarithmetic-progressionscombinatoricserdos-problems
Let be a binary relation on with no monotone -term AP (there are no and with and ) and with Ho's property : for all and . Let be a bijection with no monotone -term AP, and let . Then the prefix word is safe for (the completion ", then all other integers in -order" contains no monotone -term AP) if and only if the cut at is -closed:
In words: for a -AP-free enumeration, safety of a prefix reduces to a single closure condition on the cut. Consequently a Ho-style construction over with a fixed completion order (a prefix-increasing chain of -safe words exhausting ) is the same thing as a -AP-free enumeration of having infinitely many -closed cuts, which isolates exactly what the fixed-order method demands beyond -AP-freeness.
Preamble
import Mathlib import Definitions.Def_Erdos195_defs
Formal statement
namespace Erdos195
theorem prefix_safe_iff_closed_cut (R : ℤ → ℤ → Prop) (hA : No3AP R) (hB : Star R)
(f : ℕ ≃ ℤ) (hf : ¬ HasMonotoneAP f 4) (N : ℕ) :
Safe R ((List.range N).map f) ↔
∀ i j : ℕ, i < j → j < N → R (f i) (f j) → N ≤ f.symm (2 * f j - f i) →
f.symm (3 * f j - 2 * f i) < N := by sorry
end Erdos195Source
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)