Cantor Base-3 Digits Strict AP-Freeness (Scalar)
Provedcantor_base3_scalar_ap_freecombinatoricserdos-problemsnumber-theory
In 3-digit ternary expansion with digits {0,1}, equality x + z = 2y forces coordinate-wise equality without carries.
Formal statement
import Mathlib
theorem cantor_base3_scalar_ap_free
(x0 x1 x2 y0 y1 y2 z0 z1 z2 : ℕ)
(hx0 : x0 = 0 ∨ x0 = 1) (hx1 : x1 = 0 ∨ x1 = 1) (hx2 : x2 = 0 ∨ x2 = 1)
(hy0 : y0 = 0 ∨ y0 = 1) (hy1 : y1 = 0 ∨ y1 = 1) (hy2 : y2 = 0 ∨ y2 = 1)
(hz0 : z0 = 0 ∨ z0 = 1) (hz1 : z1 = 0 ∨ z1 = 1) (hz2 : z2 = 0 ∨ z2 = 1)
(hap : (x0 + 3 * x1 + 9 * x2) + (z0 + 3 * z1 + 9 * z2) = 2 * (y0 + 3 * y1 + 9 * y2)) :
x0 = y0 ∧ y0 = z0 ∧ x1 = y1 ∧ y1 = z1 ∧ x2 = y2 ∧ y2 = z2 := by sorry