Odd-entry demand for root-releasing tree-safe words starting with 0
ProvedErdos195.odd_entry_demandA 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. Let be a -safe word whose first letter is and which is a true root release. Then for every odd letter of :
Moreover, if has an odd letter, then some odd letter is grounded: and occurs before . Thus every odd letter starts a forced chain that must end at a grounded letter whose double is placed earlier; this is the basic necessary condition for releasing the root after a prefix, e.g. after the letters and are forced (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 odd_entry_demand (θ : ℕ → ℤ → Bool) (Q : List ℤ) (hS : Safe (treeLt θ) Q)
(h0 : Q.head? = some 0)
(hrel : ∀ a b : ℤ, a ∈ Q → b ∈ Q → Q.idxOf a < Q.idxOf b → 2 * b - a ∉ Q →
3 * b - 2 * a ∉ Q → (b - a) % 2 = 1 → b % 2 = 0) :
(∀ z ∈ Q, z % 2 = 1 →
(2 * z ∈ Q ∨ 3 * z ∈ Q) ∧ (3 * z ∉ Q → 2 * z ∈ Q ∧ Q.idxOf (2 * z) < Q.idxOf z)) ∧
((∃ z ∈ Q, z % 2 = 1) →
∃ z ∈ Q, z % 2 = 1 ∧ 3 * z ∉ Q ∧ 2 * z ∈ Q ∧ Q.idxOf (2 * z) < Q.idxOf z) := by sorry
end Erdos195