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.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

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.