Cantor base-3 3-digit strict AP-freeness
Provedcantor_base3_3digit_ap_freecombinatoricserdos-problemsnumber-theory
Cantor ternary expansion digits in {0,1} prevent 3-term arithmetic progressions.
Formal statement
import Mathlib
theorem cantor_base3_3digit_ap_free (x y z : Fin 3 → ℕ)
(hx : ∀ i, x i = 0 ∨ x i = 1)
(hy : ∀ i, y i = 0 ∨ y i = 1)
(hz : ∀ i, z i = 0 ∨ z i = 1)
(hap : (x 0 + 3 * x 1 + 9 * x 2) + (z 0 + 3 * z 1 + 9 * z 2) = 2 * (y 0 + 3 * y 1 + 9 * y 2)) :
(∀ i, x i = y i ∧ y i = z i) := by sorry