structure TournamentHamilton.Tournament (V : Type u_1) : Type u_1

A tournament on an arbitrary vertex type $V$: an irreflexive, asymmetric, and complete Boolean edge relation (between distinct vertices exactly one direction holds).

• edge : V → V → Bool
• edge_irrefl (v : V) : self.edge v v = false
• edge_complete (u v : V) : u ≠ v → self.edge u v = true ∨ self.edge v u = true
• edge_asymm (u v : V) : self.edge u v = true → self.edge v u = false

def TournamentHamilton.Tournament.IsHamiltonPath {n : ℕ} (T : Tournament (Fin n)) (σ : Equiv.Perm (Fin n)) : Prop

A permutation $\sigma$ of $\mathrm{Fin}\, n$ encodes a Hamilton path of $T$ if each consecutive directed edge $\sigma(i) \to \sigma(i+1)$ lies in $T$.

def TournamentHamilton.Tournament.IsHamiltonCycle {n : ℕ} (T : Tournament (Fin n)) (σ : Equiv.Perm (Fin n)) : Prop

A permutation $\sigma$ encodes a Hamilton cycle of $T$ if every cyclic directed edge $\sigma(i) \to \sigma((i+1) \bmod n)$ lies in $T$.

@[implicit_reducible]

instance TournamentHamilton.instDecidablePredPermFinIsHamiltonPath {n : ℕ} (T : Tournament (Fin n)) : DecidablePred T.IsHamiltonPath

Decidability of being a Hamilton path.

@[implicit_reducible]

instance TournamentHamilton.instDecidablePredPermFinIsHamiltonCycle {n : ℕ} (T : Tournament (Fin n)) : DecidablePred T.IsHamiltonCycle

Decidability of being a Hamilton cycle.

noncomputable def TournamentHamilton.Tournament.hamiltonPaths {n : ℕ} (T : Tournament (Fin n)) : Finset (Equiv.Perm (Fin n))

The finset of all Hamilton-path permutations of $T$.

noncomputable def TournamentHamilton.Tournament.hamiltonCycles {n : ℕ} (T : Tournament (Fin n)) : Finset (Equiv.Perm (Fin n))

The finset of all Hamilton-cycle permutations of $T$.

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

Number of Hamilton paths of $T$.

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

Number of Hamilton cycles of $T$.

def TournamentHamilton.extendTournament {n : ℕ} (T : Tournament (Fin n)) (f : Fin n → Bool) : Tournament (Fin (n + 1))

Extension of a tournament on $\mathrm{Fin}\, n$ to one on $\mathrm{Fin}(n+1)$ by adding a new vertex whose incoming/outgoing edges are dictated by a Boolean function $f$: $f(v) = \mathrm{true}$ means new vertex beats $v$.

theorem TournamentHamilton.card_filter_two_constraints {n : ℕ} (a b : Fin n) (hab : a ≠ b) (hn : n ≥ 2) : {f : Fin n → Bool | f a = true ∧ f b = false}.card = 2 ^ (n - 2)

The number of Boolean functions $f : \mathrm{Fin}\, n \to \{\bot, \top\}$ with $f(a) = \top$ and $f(b) = \bot$ is exactly $2^{n-2}$.

theorem TournamentHamilton.card_good_orientations {n : ℕ} (σ : Equiv.Perm (Fin n)) (hn : n ≥ 2) : {f : Fin n → Bool | f (σ ⟨0, ⋯⟩) = true ∧ f (σ ⟨n - 1, ⋯⟩) = false}.card = 2 ^ (n - 2)

For a permutation $\sigma$, the number of orientation functions $f$ making the new vertex compatible with $\sigma$ (i.e. $f(\sigma(0)) = \top$ and $f(\sigma(n-1)) = \bot$) is $2^{n-2}$.

theorem TournamentHamilton.good_paths_le_cycles (n : ℕ) (hn : n ≥ 2) (T : Tournament (Fin n)) (f : Fin n → Bool) : {σ ∈ T.hamiltonPaths | f (σ ⟨0, ⋯⟩) = true ∧ f (σ ⟨n - 1, ⋯⟩) = false}.card ≤ numHamiltonCycles (extendTournament T f)

Injection from Hamilton paths compatible with $f$ into Hamilton cycles of the extended tournament: each such path can be closed into a cycle via the new vertex.

theorem TournamentHamilton.sum_cycles_lower_bound (n : ℕ) (hn : n ≥ 2) (T : Tournament (Fin n)) : numHamiltonPaths T * 2 ^ (n - 2) ≤ ∑ f : Fin n → Bool, numHamiltonCycles (extendTournament T f)

Double-counting bound: summing the number of Hamilton cycles of each extension $T[f]$ over all orientation functions $f : \mathrm{Fin}\, n \to \{\bot, \top\}$ gives at least $\mathrm{numHamiltonPaths}(T) \cdot 2^{n-2}$.

theorem TournamentHamilton.tournament_add_vertex_hamilton_cycles (n : ℕ) (hn : n ≥ 2) (T : Tournament (Fin n)) : ∃ (T' : Tournament (Fin (n + 1))), 4 * numHamiltonCycles T' ≥ numHamiltonPaths T

Averaging argument (key step in Alon's bound for Hamilton paths): for any tournament $T$ on $n \ge 2$ vertices, there exists a one-vertex extension $T'$ on $n + 1$ vertices with $4 \cdot \mathrm{numHamiltonCycles}(T') \ge \mathrm{numHamiltonPaths}(T)$.