Among with odd, only the shield is tree-safe
ProvedErdos195.odd_shield_uniqueA tree witness is a function on the nodes , , of the binary tree of residues. For distinct integers with , put iff (two's-complement digits). 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; it is tree-safe if it is -safe for some . An in-order pair of ( occurs before ) is open if and ; an open pair lies at the node , , and -safety requires there. Let be an odd integer with . Then the four-letter word is tree-safe if and only if
i.e. the shield is the only tree-safe word of this shape. For the in-order -AP has its fourth term too late; otherwise the open pairs and conflict at the root node .
Formalization note: treeLt θ is from Definitions.Def_Erdos195_tree; Safe, bitOne are from Definitions.Def_Erdos195_defs. Positions in a word are List.idxOf; P ++ [c] appends c.
import Mathlib import Definitions.Def_Erdos195_tree
namespace Erdos195
theorem odd_shield_unique (m : ℤ) (hm : m % 2 = 1) (hm0 : 1 + m ≠ 0) :
(∃ θ : ℕ → ℤ → Bool, Safe (treeLt θ) [0, 1, 1 + m, 3]) ↔ m = 5 := by sorry
end Erdos195