Concatenating the batches and is not tree-safe
ProvedErdos195.B0_then_B1_not_safeA 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. No tree witness makes the -letter word safe. This is followed by the batch of . The in-order -AP has its completion missing from the word, which already violates safety. So the batches cannot simply be stacked.
Formalization note: treeLt θ is from Definitions.Def_Erdos195_tree; Safe, bitOne are from Definitions.Def_Erdos195_defs. Positions are List.idxOf; the release property is stated as: every open in-order pair with has .
import Mathlib import Definitions.Def_Erdos195_tree
namespace Erdos195
theorem B0_then_B1_not_safe :
¬ ∃ θ : ℕ → ℤ → Bool, Safe (treeLt θ)
[0, 1, 6, 3, -8, -2, -1, -70, -78, -36, -40, -34, -17, -230, -270, -132] := by sorry
end Erdos195