Szekeres Cantor base-3 AP-free digit rigidity

Proved

Erdos142.cantor_digit_01_no_3_ap

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

namespace Erdos142

theorem cantor_digit_01_no_3_ap (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

end Erdos142

View graph