import Mathlib.Combinatorics.Digraph.Basic
import Mathlib.GroupTheory.Perm.Cycle.Type
import Mathlib.GroupTheory.Perm.Sign
import Mathlib.Tactic

/-!
# Jackson Hamilton-decomposition counterexample

This file fixes the standard semantic vocabulary for the project. The explicit
candidate is defined in `Graph.lean`, and the exact endpoint is proved in
`Parity.lean`.
-/

namespace JacksonHamiltonDecomposition

/-- Four cyclic layers, each with labels `x`, `y`, and `z`. -/
abbrev Vertex := Fin 4 × Fin 3

/-- The proposed bipartition places even and odd layer indices on opposite sides. -/
def OppositeSides (u v : Vertex) : Prop :=
  u.1.val % 2 ≠ v.1.val % 2

/--
`T` is an orientation of the complete bipartite graph determined by
`OppositeSides`: exactly one directed arc occurs across the bipartition and no
arc occurs within either side.
-/
def IsBipartiteTournament (T : Digraph Vertex) : Prop :=
  (∀ u v, OppositeSides u v → (T.Adj u v ↔ ¬ T.Adj v u)) ∧
  (∀ u v, ¬ OppositeSides u v → ¬ T.Adj u v)

/-- Finite outdegree, defined directly because the current `Digraph` API is relation-based. -/
noncomputable def outdegree (T : Digraph Vertex) (u : Vertex) : ℕ := by
  classical
  exact (Finset.univ.filter fun v => T.Adj u v).card

/-- Finite indegree, defined directly because the current `Digraph` API is relation-based. -/
noncomputable def indegree (T : Digraph Vertex) (v : Vertex) : ℕ := by
  classical
  exact (Finset.univ.filter fun u => T.Adj u v).card

/-- Every vertex has three incoming and three outgoing arcs. -/
noncomputable def IsThreeRegular (T : Digraph Vertex) : Prop :=
  ∀ v, outdegree T v = 3 ∧ indegree T v = 3

/--
A directed Hamilton cycle is represented by its successor permutation. It is
one permutation cycle, moves every vertex, and every successor step is an arc
of `T`.
-/
def IsDirectedHamiltonCycle (T : Digraph Vertex)
    (σ : Equiv.Perm Vertex) : Prop :=
  σ.IsCycle ∧
  σ.support = Finset.univ ∧
  ∀ v, T.Adj v (σ v)

/--
An indexed family of directed Hamilton cycles partitions every arc of `T`
exactly once.
-/
def IsHamiltonDecomposition (T : Digraph Vertex) {k : ℕ}
    (C : Fin k → Equiv.Perm Vertex) : Prop :=
  (∀ i, IsDirectedHamiltonCycle T (C i)) ∧
  ∀ u v, T.Adj u v ↔ ∃! i, C i u = v

/-- `T` has a finite Hamilton decomposition, with the number of cycles not fixed in advance. -/
def HasHamiltonDecomposition (T : Digraph Vertex) : Prop :=
  ∃ k : ℕ, ∃ C : Fin k → Equiv.Perm Vertex,
    IsHamiltonDecomposition T C

/--
The exact endpoint predicate: a 3-regular bipartite tournament with no
Hamilton decomposition.
-/
noncomputable def CounterexampleStatement (T : Digraph Vertex) : Prop :=
  IsBipartiteTournament T ∧
  IsThreeRegular T ∧
  ¬ HasHamiltonDecomposition T

end JacksonHamiltonDecomposition