structure TournamentHamiltonPaths.Tournament (n : ℕ) : Type

A tournament on $n$ vertices: an irreflexive, complete, asymmetric directed-edge relation on $\mathrm{Fin}\, n$, equipped with a decidability instance.

• edge : Fin n → Fin n → Prop
• irrefl (i : Fin n) : ¬self.edge i i
• complete (i j : Fin n) : i ≠ j → self.edge i j ∨ self.edge j i
• antisymm (i j : Fin n) : self.edge i j → ¬self.edge j i
• decEdge : DecidableRel self.edge

noncomputable def TournamentHamiltonPaths.Tournament.numHamiltonPaths {n : ℕ} (T : Tournament n) : ℕ

Number of Hamilton paths of $T$: permutations $\sigma$ of $\mathrm{Fin}\, n$ such that every consecutive edge $\sigma(i) \to \sigma(i+1)$ lies in $T$.

noncomputable def TournamentHamiltonPaths.Tournament.numHamiltonCycles {n : ℕ} (T : Tournament n) : ℕ

Number of Hamilton cycles of $T$: permutations $\sigma$ of $\mathrm{Fin}(n+1)$ such that every cyclic edge $\sigma(i) \to \sigma(i+1)$ lies in $T$; zero if $n = 0$.

theorem TournamentHamiltonPaths.numHamiltonPaths_le_factorial {n : ℕ} (T : Tournament n) : T.numHamiltonPaths ≤ n.factorial

Trivial bound: the number of Hamilton paths is at most $n!$, the total number of permutations of $\mathrm{Fin}\, n$.

noncomputable def TournamentHamiltonPaths.Tournament.adjMatrix {n : ℕ} (T : Tournament n) : Matrix (Fin n) (Fin n) ℝ

Adjacency matrix of a tournament as a real $0/1$-matrix: entry $(i, j)$ is $1$ if $T$ has the edge $i \to j$, else $0$.

theorem TournamentHamiltonPaths.Tournament.adjMatrix_zero_one {n : ℕ} (T : Tournament n) (i j : Fin n) : T.adjMatrix i j = 0 ∨ T.adjMatrix i j = 1

Every entry of the tournament's adjacency matrix is $0$ or $1$.

noncomputable def TournamentHamiltonPaths.toSuccPerm {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) : Equiv.Perm (Fin (n + 1))

Successor permutation derived from $\sigma$: the conjugate $\sigma \circ (+1) \circ \sigma^{-1}$, which sends $\sigma(j)$ to $\sigma(j + 1)$.

theorem TournamentHamiltonPaths.successor_relation {n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) (j : Fin (n + 1)) : σ (j + 1) = (toSuccPerm σ) (σ j)

Successor relation: $\sigma(j + 1) = (\mathrm{toSuccPerm}\,\sigma)(\sigma(j))$.

theorem TournamentHamiltonPaths.toSuccPerm_valid {n : ℕ} (T : Tournament (n + 1)) (σ : Equiv.Perm (Fin (n + 1))) (hσ : ∀ (i : Fin (n + 1)), T.edge (σ i) (σ (i + 1))) (v : Fin (n + 1)) : T.edge v ((toSuccPerm σ) v)

If $\sigma$ encodes a Hamilton cycle of $T$, then for every vertex $v$ the directed edge $v \to (\mathrm{toSuccPerm}\,\sigma)(v)$ lies in $T$.

theorem TournamentHamiltonPaths.fiber_eq_of_eq_at_zero {n : ℕ} (σ₁ σ₂ : Equiv.Perm (Fin (n + 1))) (heq : toSuccPerm σ₁ = toSuccPerm σ₂) (h0 : σ₁ 0 = σ₂ 0) : σ₁ = σ₂

Two permutations with the same successor permutation and the same value at $0$ must be equal: induct on the index using the successor relation.

theorem TournamentHamiltonPaths.permanent_ge_card_row {m : ℕ} (A : Matrix (Fin m) (Fin m) ℝ) (hA : ∀ (i j : Fin m), A i j = 0 ∨ A i j = 1) (S : Finset (Equiv.Perm (Fin m))) (hS : ∀ σ ∈ S, ∀ (i : Fin m), A (σ i) i = 1) : ↑S.card ≤ A.permanent

Permanent lower bound: if $S$ is a set of permutations $\sigma$ with $A_{\sigma(i), i} = 1$ for all $i$, then $\mathrm{perm}(A) \ge |S|$.

theorem TournamentHamiltonPaths.adjMatrix_entry_one_iff {m : ℕ} (T : Tournament m) (i j : Fin m) : T.adjMatrix i j = 1 ↔ T.edge i j

Adjacency-matrix entry is $1$ iff the corresponding tournament edge exists.

theorem TournamentHamiltonPaths.numHamiltonCycles_le_mul_permanent {n : ℕ} (T : Tournament (n + 1)) : ↑T.numHamiltonCycles ≤ (↑n + 1) * T.adjMatrix.permanent

Key counting bound: the number of Hamilton cycles is at most $(n + 1) \cdot \mathrm{perm}(A_T)$, where $A_T$ is the adjacency matrix of $T$.

theorem TournamentHamiltonPaths.tournament_permanent_optimization_bound {n : ℕ} (T : Tournament (n + 1)) : ↑(n + 1) * T.adjMatrix.permanent ≤ √(Real.pi / 2 + 1) * √↑(n + 1) * ↑(n + 1).factorial / 2 ^ (n + 1)

Permanent optimization bound for tournament adjacency matrices: combining Brégman's inequality with smoothing/Stirling, $(n + 1) \cdot \mathrm{perm}(A_T) \le \sqrt{\pi/2 + 1} \cdot \sqrt{n+1} \cdot (n+1)! / 2^{n+1}$.

theorem TournamentHamiltonPaths.hamilton_cycles_upper_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ) (T : Tournament n), ↑T.numHamiltonCycles ≤ C * √↑n * ↑n.factorial / 2 ^ n

Alon's Hamilton-cycle bound: there exists $C > 0$ such that every $n$-vertex tournament has at most $C \sqrt{n} \cdot n! / 2^n$ Hamilton cycles.

theorem TournamentHamiltonPaths.hamilton_paths_to_cycles {n : ℕ} (hn : 2 ≤ n) (T : Tournament n) : ∃ (T' : Tournament (n + 1)), T.numHamiltonPaths ≤ 4 * T'.numHamiltonCycles

Averaging step: for $n \ge 2$ there exists a one-vertex extension $T'$ of $T$ such that $\mathrm{numHamiltonPaths}(T) \le 4 \cdot \mathrm{numHamiltonCycles}(T')$.

theorem TournamentHamiltonPaths.alon_hamilton_paths_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (T : Tournament n), ↑T.numHamiltonPaths ≤ C * ↑n * √↑n * ↑n.factorial / 2 ^ n

Theorem 10.2.4 (Alon 1990, Hamilton paths). There exists $C > 0$ such that every $n$-vertex tournament has at most $C \cdot n \sqrt{n} \cdot n! / 2^n$ Hamilton paths.