Injectivity of the three-paths path parametrisation

Proved

MetricTSP.three_paths_seq_inj

by Shuze Chen · Aug 24, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatorial-optimizationgraph-theorytraveling-salesman-problem

The parametrisation of the three-parallel-paths instance by (path, step) is injective away from the hubs. The instance on $n = 3k+2$ cities has two hubs $s$ (index $0$ ) and $t$ (index $3k+1$ ) joined by three internally disjoint paths of $k$ internal cities each; tpSeq k p m is the $m$ -th city along path $p$ , i.e. $s$ for $m = 0$ , $t$ for $m = k+1$ , and the internal city with index $1 + pk + (m-1)$ for $1 \le m \le k$ .

If the $m$ -th city of path $p$ coincides with the $m_2$ -th city of path $q$ (with $p, q < 3$ and $m, m_2 \le k+1$ ), then $m = m_2$ , and moreover either $p = q$ or the common step is a hub step ( $m = 0$ or $m = k+1$ ).

The proof is index arithmetic: the internal index $1 + pk + (m-1)$ lies strictly between $0$ and $3k+1$ and determines $(p, m)$ uniquely by division with remainder, while the hubs occupy the extreme indices. This injectivity underlies the cut analysis of the fractional certificate in the $4/3$ integrality-gap construction (MetricTSP.three_paths_cert_feasible).

Preamble

import Mathlib
import Definitions.Def_MetricTSP_model
import Definitions.Def_MetricTSP_three_paths

Formal statement

namespace MetricTSP

/-- The `m`-th city along path `p` of the three-paths instance: the hub `s` at
`m = 0`, the hub `t` at `m = k+1`, and the internal cities in between. -/
def tpSeq (k p m : ℕ) : Fin (3*k+2) :=
  if m = 0 then ⟨0, by omega⟩
  else if m = k+1 then ⟨3*k+1, by omega⟩
  else ⟨(1 + p*k + (m-1)) % (3*k+2), Nat.mod_lt _ (by omega)⟩

theorem three_paths_seq_inj (k : ℕ) (hk : 1 ≤ k) (p q m m2 : ℕ)
    (hp : p < 3) (hq : q < 3) (hm : m ≤ k+1) (hm2 : m2 ≤ k+1)
    (h : tpSeq k p m = tpSeq k q m2) :
    m = m2 ∧ (p = q ∨ m = 0 ∨ m = k+1) := by sorry

end MetricTSP

Source

G. Benoit, S. Boyd, Finding the exact integrality gap for small traveling salesman problems, Mathematics of Operations Research 33 (2008) 921-931 (the three-paths family); folklore index arithmetic.

View graph