@[reducible, inline]

abbrev SzeleTournament.EdgeSet (n : ℕ) : Type

The set of unordered edge positions on $n$ labeled vertices, encoded as ordered pairs $(i, j)$ with $i < j$.

@[reducible, inline]

abbrev SzeleTournament.Tournament (n : ℕ) : Type

A tournament on $n$ vertices: an orientation assigning a Boolean direction to each unordered edge in EdgeSet n.

def SzeleTournament.tournamentEdge {n : ℕ} (T : Tournament n) (i j : Fin n) : Bool

The directed edge from $i$ to $j$ in tournament $T$: true if $T$ orients the edge in the direction $i \to j$, false otherwise (including the diagonal).

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

A permutation $\sigma$ of $\mathrm{Fin}\,n$ is a Hamilton path in tournament $T$ if every consecutive pair $(\sigma(i), \sigma(i+1))$ is a directed edge of $T$.

@[implicit_reducible]

instance SzeleTournament.instDecIsHP {n : ℕ} (T : Tournament n) (σ : Equiv.Perm (Fin n)) : Decidable (IsHamiltonPath T σ)

Decidability instance for IsHamiltonPath, used for counting.

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

The number of Hamilton paths in a tournament $T$, defined as the cardinality of the set of permutations $\sigma$ for which IsHamiltonPath T σ holds.

theorem SzeleTournament.card_fiber_hp {n : ℕ} (σ : Equiv.Perm (Fin n)) (hn : n ≥ 1) : {T : Tournament n | IsHamiltonPath T σ}.card = 2 ^ (Fintype.card (EdgeSet n) - (n - 1))

For a fixed permutation $\sigma$, the number of tournaments in which $\sigma$ is a Hamilton path equals $2^{|E| - (n-1)}$, since the $n-1$ consecutive edges along $\sigma$ must be oriented in a unique direction while the remaining edges are free.

theorem SzeleTournament.n_sub_one_le_card_edgeset (n : ℕ) (hn : n ≥ 1) : n - 1 ≤ Fintype.card (EdgeSet n)

For $n \geq 1$, the edge count of EdgeSet n is at least $n - 1$, exhibited by the path $(0,1), (1,2), \dots, (n-2, n-1)$.

theorem SzeleTournament.total_sum_hp (n : ℕ) (hn : n ≥ 1) : ∑ T : Tournament n, numHamiltonPaths T = n.factorial * 2 ^ (Fintype.card (EdgeSet n) - (n - 1))

Total count via double counting: summing the number of Hamilton paths over all tournaments equals $n! \cdot 2^{|E| - (n-1)}$, because for each of the $n!$ permutations exactly $2^{|E| - (n-1)}$ tournaments admit it as a Hamilton path.

theorem SzeleTournament.szele_hamilton_paths (n : ℕ) (hn : n ≥ 1) : ∃ (T : Tournament n), n.factorial ≤ numHamiltonPaths T * 2 ^ (n - 1)

Szele's theorem (Theorem 2.1.2, 1943). For every $n \geq 1$ there exists a tournament on $n$ vertices with at least $n! / 2^{n-1}$ Hamilton paths.