A true root release after the prefix (0,1,9): the word (0,1,9,3,54,27)
ProvedErdos195.nine_true_releaseA 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. An in-order pair of ( occurs before ) is open if and ; it lies at the node , , and forces there to equal . A root pair is one with odd (node ); is a true root release if every open root pair has even second entry, i.e. no open pair forces the value at the root. The six-letter word
is tree-safe (with the witness for and ) and is a true root release: its open root pairs all have even second entry. Hence the root can be released after the three-letter prefix . Here the forced -chains of the odd letters and merge (), so a single grounded letter (preceded by ) suffices; for a general odd third letter the chains of and are disjoint and at least two grounded letters are needed (Erdős Problem 195, tree-witness approach).
Formalization note: treeLt θ is from Definitions.Def_Erdos195_tree; Safe, bitOne are from Definitions.Def_Erdos195_defs. Positions are List.idxOf; "starts with 0" is Q.head? = some 0; the release hypothesis is stated as: every open in-order pair with has .
import Mathlib import Definitions.Def_Erdos195_tree
namespace Erdos195
theorem nine_true_release :
(∃ θ : ℕ → ℤ → Bool, Safe (treeLt θ) [0, 1, 9, 3, 54, 27]) ∧
∀ a b : ℤ, a ∈ [0, 1, 9, 3, 54, 27] → b ∈ [0, 1, 9, 3, 54, 27] →
[0, 1, 9, 3, 54, 27].idxOf a < [0, 1, 9, 3, 54, 27].idxOf b →
2 * b - a ∉ [0, 1, 9, 3, 54, 27] → 3 * b - 2 * a ∉ [0, 1, 9, 3, 54, 27] →
(b - a) % 2 = 1 → b % 2 = 0 := by sorry
end Erdos195