A tour is a cyclic enumeration

DescriptiveComplexity.TourOn reads a Hamilton circuit as a linear order of the universe, which is what an existential second-order block can guess. This file shows that reading is the intended one: a tour is exactly a cyclic enumeration of the universe along which consecutive elements are adjacent (DescriptiveComplexity.tourOn_iff_enum).

Both halves are what a reduction into either Hamilton problem consumes. A gadget builds its circuit as an explicit enumeration and needs DescriptiveComplexity.tourOn_of_enum; conversely it reads a given circuit through the cyclic successor f (nextIdx i) (DescriptiveComplexity.enum_of_tourOn), whose local structure – every vertex is left once and reached once – is what forces a gadget to be traversed the intended way.

def DescriptiveComplexity.nextIdx {n : ℕ} (i : Fin n) : Fin n

The next index, cyclically: the last one wraps around to the first.

Equations

• DescriptiveComplexity.nextIdx i = ⟨(↑i + 1) % n, ⋯⟩

theorem DescriptiveComplexity.tourOn_of_enum {A : Type} {R : A → A → Prop} {n : ℕ} (f : Fin n ≃ A) (h : ∀ (i : Fin n), R (f i) (f (nextIdx i))) : TourOn R

An enumeration is a tour: order the universe by the position of each element.

theorem DescriptiveComplexity.enum_of_tourOn {A : Type} [Finite A] {R : A → A → Prop} (h : TourOn R) : ∃ (n : ℕ) (f : Fin n ≃ A), ∀ (i : Fin n), R (f i) (f (nextIdx i))

A tour is an enumeration: reading the universe along the order the tour carries lists every element exactly once, consecutive ones being adjacent, and the last one adjacent to the first.

theorem DescriptiveComplexity.tourOn_iff_enum {A : Type} [Finite A] {R : A → A → Prop} : TourOn R ↔ ∃ (n : ℕ) (f : Fin n ≃ A), ∀ (i : Fin n), R (f i) (f (nextIdx i))

A tour is exactly a cyclic enumeration: the two readings of a Hamilton circuit agree.