Fourth-term completion of an extremal open pair keeps the forced node value
ProvedErdos195.immediate_fourth_term_persistA 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 open in-order pair of a finite word , let , and suppose is the numerical maximum or the numerical minimum of the letters of congruent to modulo . Put . Then in the word the pair is in order and open, lies at the same node as , and forces the same value:
So completing an extremal open pair by its fourth term never releases the node it was forcing; the forced value persists (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 in a word are List.idxOf; P ++ [c] appends c.
import Mathlib import Definitions.Def_Erdos195_tree
namespace Erdos195
theorem immediate_fourth_term_persist (P : List ℤ) (u w : ℤ) (hu : u ∈ P) (hw : w ∈ P)
(hord : P.idxOf u < P.idxOf w) (h2 : 2 * w - u ∉ P) (h3 : 3 * w - 2 * u ∉ P)
(hext : (∀ x ∈ P, (2 : ℤ) ^ padicValInt 2 (w - u) ∣ x - w → x ≤ w) ∨
(∀ x ∈ P, (2 : ℤ) ^ padicValInt 2 (w - u) ∣ x - w → w ≤ x)) :
u ∈ P ++ [3 * w - 2 * u] ∧ 3 * w - 2 * u ∈ P ++ [3 * w - 2 * u] ∧
(P ++ [3 * w - 2 * u]).idxOf u < (P ++ [3 * w - 2 * u]).idxOf (3 * w - 2 * u) ∧
2 * (3 * w - 2 * u) - u ∉ P ++ [3 * w - 2 * u] ∧
3 * (3 * w - 2 * u) - 2 * u ∉ P ++ [3 * w - 2 * u] ∧
padicValInt 2 ((3 * w - 2 * u) - u) = padicValInt 2 (w - u) ∧
(bitOne (3 * w - 2 * u) (padicValInt 2 (w - u)) ↔ bitOne w (padicValInt 2 (w - u))) := by sorry
end Erdos195