Circuits, locally and from a potential

Two readings of a Hamilton circuit (DescriptiveComplexity.IsCircuit) that never mention the linear order it is a cut of, for the two halves of a reduction into a circuit problem.

• What a circuit gives (DescriptiveComplexity.IsCircuit.local): every vertex is left once and reached once, along the relation, and two vertices that follow each other both ways are the whole universe. That is all a gadget argument uses: which arc leaves a vertex is settled by which arcs can still reach its neighbours.
• What makes a circuit (DescriptiveComplexity.isCircuit_of_potential): a relation along which every vertex is left once and reached once is a circuit as soon as some potential strictly increases along it at every vertex but one. An orbit avoiding that vertex could never close, so there is one orbit. The order is then read off the powers of the permutation, and the potential is checked arc by arc: no enumeration of the circuit has to be written.

theorem DescriptiveComplexity.cycSucc_reverse {V : Type} {Le : V → V → Prop} {x y : V} : CycSucc (fun (a b : V) => Le b a) x y ↔ CycSucc Le y x

The cyclic successor of the reverse order is the cyclic predecessor.

theorem DescriptiveComplexity.IsCircuit.reverse {V : Type} {R Nxt : V → V → Prop} (hsym : ∀ (x y : V), R x y → R y x) (h : IsCircuit R Nxt) : IsCircuit R fun (x y : V) => Nxt y x

A circuit of a symmetric relation, traversed backwards, is a circuit.

theorem DescriptiveComplexity.IsCircuit.induction {V : Type} [Finite V] {R Nxt : V → V → Prop} (h : IsCircuit R Nxt) {P : V → Prop} (x₀ : V) (h0 : P x₀) (hstep : ∀ (x y : V), Nxt x y → P x → P y) (x : V) : P x

Induction along a circuit: a property of one vertex that passes to the next vertex holds of every vertex.

theorem DescriptiveComplexity.IsCircuit.local {V : Type} [Finite V] {R Nxt : V → V → Prop} (h : IsCircuit R Nxt) : (∀ (x : V), ∃ (y : V), Nxt x y) ∧ (∀ (x y y' : V), Nxt x y → Nxt x y' → y = y') ∧ (∀ (y : V), ∃ (x : V), Nxt x y) ∧ (∀ (x x' y : V), Nxt x y → Nxt x' y → x = x') ∧ (∀ (x y : V), Nxt x y → R x y) ∧ ∀ (x y : V), Nxt x y → Nxt y x → ∀ (z : V), z = x ∨ z = y

A circuit, read locally: every vertex is left once and reached once, along the relation, and two vertices following each other both ways are the whole universe.

theorem DescriptiveComplexity.isCircuit_of_potential {V : Type} [Finite V] {K : Type} [Preorder K] {R Nxt : V → V → Prop} (htot : ∀ (x : V), ∃ (y : V), Nxt x y) (hfun : ∀ (x y y' : V), Nxt x y → Nxt x y' → y = y') (hsurj : ∀ (y : V), ∃ (x : V), Nxt x y) (hR : ∀ (x y : V), Nxt x y → R x y) (key : V → K) (v₀ : V) (hkey : ∀ (x y : V), Nxt x y → x ≠ v₀ → key x < key y) : IsCircuit R Nxt

A circuit from a potential: a relation along which every vertex is left once and reached once, included in R, is a Hamilton circuit of R as soon as some potential strictly increases along it at every vertex but one.