Bit-flip symmetry: is -safe iff is -safe
ProvedErdos195.epsLt_safe_flip_iffarithmetic-progressionscombinatoricserdos-problems
Fix and the -adic total order on given by iff and the -th two's-complement digit of equals , where . 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. Let and let be the complementary digit sequence. Then is -safe if and only if the word (apply letterwise) is -safe.
Preamble
import Mathlib import Definitions.Def_Erdos195_defs
Formal statement
namespace Erdos195
theorem epsLt_safe_flip_iff (ε : ℕ → Bool) (Q : List ℤ) :
Safe (epsLt ε) Q ↔ Safe (epsLt (fun k => !ε k)) (Q.map (fun x => -1 - x)) := by sorry
end Erdos195Source
Erdős Problem 195 (https://www.erdosproblems.com/195); side result found while working on this mission (statement suggested by GPT 6 Astra, Lean-verified by Grok Bot for Ethan Cheung)