Truncated distances, and the duplicator's answer on a line

The arithmetic core of the Ehrenfeucht–Fraïssé game on linear orders (Ehrenfeucht 1961; Ebbinghaus–Flum 1995, ch. 2): no logic and no game here, only integers.

The duplicator's invariant on a line is the classical one – corresponding points are at equal distance, or at distance at least 2 ^ n on both sides, where n is the number of rounds still to play. Written with the truncation DescriptiveComplexity.truncAt n – clamping to [-2 ^ n, 2 ^ n] – the two alternatives, the order between the points and the case of equal points all become the single equation truncAt n (x - y) = truncAt n (x' - y') (DescriptiveComplexity.truncAt_eq_iff), which is what makes the invariant manageable: one clause instead of four.

The theorem of the file is DescriptiveComplexity.exists_answer: from an invariant with n + 1 rounds to spare, any point the spoiler picks between two existing points can be answered so that the invariant holds with n rounds. Its proof is the textbook case analysis – copy the distance to the left neighbor, or to the right one, or, when both are large, land in the middle of a gap that the invariant guarantees is twice as large on the other side – with the halving of the budget appearing exactly there.

Truncation

def DescriptiveComplexity.truncAt (n : ℕ) (x : ℤ) : ℤ

The distance truncated at 2 ^ n: an integer clamped to [-2 ^ n, 2 ^ n]. Two truncated distances are equal exactly when the distances are equal or both beyond the truncation, on the same side (DescriptiveComplexity.truncAt_eq_iff).

Equations

• DescriptiveComplexity.truncAt n x = max (-2 ^ n) (min (2 ^ n) x)

theorem DescriptiveComplexity.two_pow_pos (n : ℕ) : 0 < 2 ^ n

theorem DescriptiveComplexity.truncAt_of_abs_le {n : ℕ} {x : ℤ} (h₁ : -2 ^ n ≤ x) (h₂ : x ≤ 2 ^ n) : truncAt n x = x

Truncation is the identity within the bounds.

theorem DescriptiveComplexity.truncAt_of_le {n : ℕ} {x : ℤ} (h : 2 ^ n ≤ x) : truncAt n x = 2 ^ n

Truncation is 2 ^ n above the bound.

theorem DescriptiveComplexity.truncAt_of_le_neg {n : ℕ} {x : ℤ} (h : x ≤ -2 ^ n) : truncAt n x = -2 ^ n

Truncation is -2 ^ n below the bound.

theorem DescriptiveComplexity.truncAt_eq_iff {n : ℕ} {x y : ℤ} : truncAt n x = truncAt n y ↔ x = y ∨ 2 ^ n ≤ x ∧ 2 ^ n ≤ y ∨ x ≤ -2 ^ n ∧ y ≤ -2 ^ n

The characterization of equal truncated distances: equal distances, or both beyond the truncation on the same side. Every property of the duplicator's invariant is read off this.

What an equation between truncated distances says

theorem DescriptiveComplexity.le_zero_congr_of_truncAt {n : ℕ} {x y : ℤ} (h : truncAt n x = truncAt n y) : x ≤ 0 ↔ y ≤ 0

Equal truncated distances have the same sign, weakly.

theorem DescriptiveComplexity.lt_zero_congr_of_truncAt {n : ℕ} {x y : ℤ} (h : truncAt n x = truncAt n y) : x < 0 ↔ y < 0

Equal truncated distances have the same strict sign.

theorem DescriptiveComplexity.neg_congr_of_truncAt {n : ℕ} {x y : ℤ} (h : truncAt n x = truncAt n y) : truncAt n (-x) = truncAt n (-y)

Truncation commutes with negation, as an equation between two distances.

theorem DescriptiveComplexity.eq_zero_congr_of_truncAt {n : ℕ} {x y : ℤ} (h : truncAt n x = truncAt n y) : x = 0 ↔ y = 0

Equal truncated distances are zero together.

theorem DescriptiveComplexity.truncAt_eq_of_le {n : ℕ} {x y : ℤ} {m : ℕ} (hmn : m ≤ n) (h : truncAt n x = truncAt n y) : truncAt m x = truncAt m y

Truncating further is coarser: an equation between distances truncated at 2 ^ n survives truncation at any smaller bound. This is how a round is spent – the budget halves, and the invariant still holds.

theorem DescriptiveComplexity.truncAt_sub_shift {n : ℕ} {x y s : ℤ} (h : truncAt (n + 1) x = truncAt (n + 1) y) (hs₁ : -2 ^ n ≤ s) (hs₂ : s ≤ 2 ^ n) : truncAt n (x - s) = truncAt n (y - s)

Shifting both sides by a small amount costs one round: two distances equal up to truncation at 2 ^ (n + 1) stay equal up to truncation at 2 ^ n after a common shift of at most 2 ^ n. This single lemma answers the spoiler in the two easy cases of DescriptiveComplexity.exists_answer – the shift being the distance from the new point to the neighbor the duplicator copies.

The duplicator's answer

theorem DescriptiveComplexity.exists_answer {n : ℕ} {ι : Type} [Finite ι] {U V : ι → ℤ} (hinv : ∀ (i i' : ι), truncAt (n + 1) (U i - U i') = truncAt (n + 1) (V i - V i')) {c : ℤ} {i₀ i₁ : ι} (h₀ : U i₀ ≤ c) (h₁ : c ≤ U i₁) : ∃ (d : ℤ), ∀ (i : ι), truncAt n (U i - c) = truncAt n (V i - d)

The duplicator answers on a line. Two families of integers whose mutual distances agree up to truncation at 2 ^ (n + 1), and a new point c lying between two points of the first family: then there is a point d answering it, whose distances to the second family agree, up to truncation at 2 ^ n, with those of c to the first.

The three cases are the classical ones: if c is one of the existing points, copy the corresponding one; if c is closer than 2 ^ n to its left or right neighbor, copy that distance (DescriptiveComplexity.truncAt_sub_shift); and if it is far from both, the gap it sits in is at least 2 ^ (n + 1) wide, hence so is the corresponding gap, and there is room to land at exactly 2 ^ n from the left neighbor.