Szekeres Cantor base-3 AP-free digit rigidity

Proved

cantor_base3_ap_free

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemsnumber-theory

Any ternary digit equation $x + z = 2y$ restricted to digits $x, y, z \in \{0, 1\}$ forces $x = z$ . This is the digit-level rigidity underlying the Szekeres Cantor-type construction of AP-free sets.

Formal statement

import Mathlib

theorem cantor_base3_ap_free (x_digit y_digit z_digit : Nat) (hx : x_digit = 0 ∨ x_digit = 1) (hy : y_digit = 0 ∨ y_digit = 1) (hz : z_digit = 0 ∨ z_digit = 1) (hap : x_digit + z_digit = 2 * y_digit) : x_digit = z_digit := by sorry

View graph