has no even-only SAFE extension containing a new entry
ProvedErdos195.H1_no_even_only_extensionarithmetic-progressionscombinatoricserdos-problems
A tree witness is a function on the nodes , , of the binary tree of residues. For distinct integers with , put iff . A finite word of integers is -safe if the sequence "the letters of in order, then all remaining integers in -order" contains no monotone -term arithmetic progression. is SAFE if it is -safe for some tree witness . Let , which is SAFE. If is a finite word of even integers, at least one of which does not occur in , then is not SAFE. (The new-entry condition is necessary: appending already present letters does not change SAFE-ness.) This is GPT Astra's preparation obstruction: any SAFE continuation of with a new even entry must also add new odd entries.
Preamble
import Mathlib import Definitions.Def_Erdos195_tree
Formal statement
namespace Erdos195
theorem H1_no_even_only_extension (D : List ℤ) (hD : ∀ z ∈ D, z % 2 = 0)
(hnew : ∃ z ∈ D, z ∉ [0, 1, -1, 5, 3, 2, -15, -11, -5, -99, -115, -55, 109, -3]) :
¬ ∃ θ : ℕ → ℤ → Bool,
Safe (treeLt θ) ([0, 1, -1, 5, 3, 2, -15, -11, -5, -99, -115, -55, 109, -3] ++ D) := by sorry
end Erdos195Source
Erdős Problem 195 (https://www.erdosproblems.com/195); tree-witness framework; construction and proof sketch by GPT Astra, Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)