Astra's four-class absorption certificate (27 letters) is SAFE
ProvedErdos195.astra_fourclass_example_safearithmetic-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 . The word
is SAFE. It is the instance , , , of the four-class absorption recipe; occupies all four residue classes modulo .
Preamble
import Mathlib import Definitions.Def_Erdos195_tree
Formal statement
namespace Erdos195
theorem astra_fourclass_example_safe :
∃ θ : ℕ → ℤ → Bool, Safe (treeLt θ)
[0, 1, 17, 49, 9, 25, 57, 41, 3, 33, 35, 19, -13, 27, 11, -21, -5, 18,
183, 151, 167, 199, 159, 175, 207, 191, 93] := 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)