2607.19276v1 / Norine/Basic.lean

all files

import Mathlib

/-!
# Norine's antipodal-coloring conjecture

This file formalizes the graph-theoretic statement and the reduction in Section 2 of
Wu--Yang, *A Chain-Level Borsuk--Ulam Obstruction Proof of Norine's
Antipodal-Coloring Conjecture*.

The two colors are represented by `Bool`; `true` is called red and `false` blue.
-/

open Function

namespace Norine

noncomputable section

/-- The vertices of the `n`-dimensional discrete cube. -/
abbrev Cube (n : ℕ) := Fin n → Bool

/-- Coordinatewise complementation, the antipodal involution of the cube. -/
def antipode {n : ℕ} (x : Cube n) : Cube n := fun i ↦ !x i

@[simp]
theorem antipode_apply {n : ℕ} (x : Cube n) (i : Fin n) :
    antipode x i = !x i := rfl

@[simp]
theorem antipode_antipode {n : ℕ} (x : Cube n) :
    antipode (antipode x) = x := by
  funext i
  simp [antipode]

theorem antipode_injective {n : ℕ} : Injective (@antipode n) :=
  fun x y h ↦ by
    rw [← antipode_antipode x, ← antipode_antipode y, h]

/-- Cube adjacency: there is one coordinate at which the vertices differ and they
agree at every other coordinate. -/
def CubeAdjacent {n : ℕ} (x y : Cube n) : Prop :=
  ∃ i : Fin n, x i ≠ y i ∧ ∀ j : Fin n, j ≠ i → x j = y j

theorem cubeAdjacent_symm {n : ℕ} : Std.Symm (@CubeAdjacent n) := by
  constructor
  rintro x y ⟨i, hi, hrest⟩
  exact ⟨i, hi.symm, fun j hji ↦ (hrest j hji).symm⟩

theorem cubeAdjacent_irrefl {n : ℕ} : Std.Irrefl (@CubeAdjacent n) := by
  constructor
  intro x
  rintro ⟨i, hi, -⟩
  exact hi rfl

/-- The usual graph of the discrete `n`-cube. -/
def cubeGraph (n : ℕ) : SimpleGraph (Cube n) where
  Adj := CubeAdjacent
  symm := cubeAdjacent_symm
  loopless := cubeAdjacent_irrefl

@[simp]
theorem cubeGraph_adj {n : ℕ} {x y : Cube n} :
    (cubeGraph n).Adj x y ↔ CubeAdjacent x y := Iff.rfl

theorem cubeAdjacent_antipode {n : ℕ} {x y : Cube n} :
    CubeAdjacent (antipode x) (antipode y) ↔ CubeAdjacent x y := by
  constructor
  · rintro ⟨i, hi, hrest⟩
    refine ⟨i, ?_, fun j hji ↦ ?_⟩
    · simpa [antipode] using hi
    · simpa [antipode] using hrest j hji
  · rintro ⟨i, hi, hrest⟩
    refine ⟨i, ?_, fun j hji ↦ ?_⟩
    · simpa [antipode] using hi
    · simpa [antipode] using hrest j hji

/-- A (symmetric) two-coloring of cube edges. Values away from edges are immaterial. -/
structure EdgeColoring (n : ℕ) where
  color : Cube n → Cube n → Bool
  symm : ∀ x y, color x y = color y x

namespace EdgeColoring

instance (n : ℕ) : CoeFun (EdgeColoring n) (fun _ ↦ Cube n → Cube n → Bool) :=
  ⟨EdgeColoring.color⟩

/-- The spanning subgraph consisting of the edges of color `b`. -/
def colorGraph {n : ℕ} (c : EdgeColoring n) (b : Bool) : SimpleGraph (Cube n) where
  Adj x y := CubeAdjacent x y ∧ c x y = b
  symm := by
    constructor
    rintro x y ⟨hxy, hc⟩
    exact ⟨cubeAdjacent_symm.symm x y hxy, by rw [← c.symm]; exact hc⟩
  loopless := by
    constructor
    exact fun x h ↦ cubeAdjacent_irrefl.irrefl x h.1

@[simp]
theorem colorGraph_adj {n : ℕ} (c : EdgeColoring n) (b : Bool) {x y : Cube n} :
    (c.colorGraph b).Adj x y ↔ CubeAdjacent x y ∧ c x y = b := Iff.rfl

/-- There is a monochromatic walk of color `b` between `x` and `y`. -/
def MonoConnected {n : ℕ} (c : EdgeColoring n) (b : Bool) (x y : Cube n) : Prop :=
  (c.colorGraph b).Reachable x y

/-- The paper's antipodality condition: antipodal edges receive opposite colors. -/
def IsAntipodal {n : ℕ} (c : EdgeColoring n) : Prop :=
  ∀ ⦃x y : Cube n⦄, CubeAdjacent x y → c (antipode x) (antipode y) = !(c x y)

end EdgeColoring

/-- A rook labeling, in the coordinate form of Definition 2.1. -/
structure RookLabeling (N r : ℕ) where
  fst : Cube N → Fin r
  snd : Cube N → Fin r
  offDiagonal : ∀ x, fst x ≠ snd x
  antipodal_fst : ∀ x, fst (antipode x) = snd x
  antipodal_snd : ∀ x, snd (antipode x) = fst x
  rook : ∀ ⦃x y⦄, CubeAdjacent x y → fst x = fst y ∨ snd x = snd y

/-- The paper's label set `Ωᵣ = {(a,b) : a ≠ b}`. -/
abbrev Omega (r : ℕ) := {p : Fin r × Fin r // p.1 ≠ p.2}

/-- Swap the two coordinates of an off-diagonal pair. -/
def omegaSwap {r : ℕ} (p : Omega r) : Omega r :=
  ⟨(p.1.2, p.1.1), p.2.symm⟩

@[simp]
theorem omegaSwap_fst {r : ℕ} (p : Omega r) : (omegaSwap p).1.1 = p.1.2 := rfl

@[simp]
theorem omegaSwap_snd {r : ℕ} (p : Omega r) : (omegaSwap p).1.2 = p.1.1 := rfl

@[simp]
theorem omegaSwap_omegaSwap {r : ℕ} (p : Omega r) : omegaSwap (omegaSwap p) = p := by
  apply Subtype.ext
  exact Prod.swap_swap p.1

/-- A literal restatement of Definition 2.1 using a map into `Ωᵣ`. -/
structure NaiveRookLabeling (N r : ℕ) where
  q : Cube N → Omega r
  antipodal : ∀ x, q (antipode x) = omegaSwap (q x)
  rook : ∀ ⦃x y⦄, CubeAdjacent x y →
    (q x).1.1 = (q y).1.1 ∨ (q x).1.2 = (q y).1.2

/-- The coordinate presentation used in the proof is equivalent to the paper's
literal `Ωᵣ`-valued presentation. -/
def rookLabelingEquivNaive (N r : ℕ) : RookLabeling N r ≃ NaiveRookLabeling N r where
  toFun q :=
    { q := fun x ↦ ⟨(q.fst x, q.snd x), q.offDiagonal x⟩
      antipodal := by
        intro x
        apply Subtype.ext
        exact Prod.ext (q.antipodal_fst x) (q.antipodal_snd x)
      rook := q.rook }
  invFun q :=
    { fst := fun x ↦ (q.q x).1.1
      snd := fun x ↦ (q.q x).1.2
      offDiagonal := fun x ↦ (q.q x).2
      antipodal_fst := by
        intro x
        exact congr_arg (fun p : Omega r ↦ p.1.1) (q.antipodal x)
      antipodal_snd := by
        intro x
        exact congr_arg (fun p : Omega r ↦ p.1.2) (q.antipodal x)
      rook := q.rook }
  left_inv q := by
    cases q
    rfl
  right_inv q := by
    cases q
    rfl

/-- A monochromatic antipodal path is exactly the conclusion of Theorem 1.1. -/
def HasMonochromaticAntipodalPath {n : ℕ} (c : EdgeColoring n) : Prop :=
  ∃ x : Cube n, ∃ b : Bool, c.MonoConnected b x (antipode x)

/-- `MonoConnected` really is the existence of a finite graph walk all of whose
edges have the selected color; this is the paper's meaning of "monochromatic path".
The standard path obtained by deleting loops from this walk has the same endpoints. -/
theorem monoConnected_iff_walk {n : ℕ} (c : EdgeColoring n) (b : Bool)
    (x y : Cube n) :
    c.MonoConnected b x y ↔ Nonempty ((c.colorGraph b).Walk x y) := Iff.rfl

/-- The exact graph-theoretic statement of Norine's conjecture. -/
def NorineConjecture : Prop :=
  ∀ n : ℕ, 2 ≤ n → ∀ c : EdgeColoring n, c.IsAntipodal →
    HasMonochromaticAntipodalPath c

/-! ## Section 2: reduction to a rook labeling -/

/-- Restrict a vertex of a larger cube to its first `n` coordinates. -/
def restrictCube (n r : ℕ) (x : Cube (n + r)) : Cube n :=
  fun i ↦ x (Fin.castAdd r i)

@[simp]
theorem restrictCube_antipode (n r : ℕ) (x : Cube (n + r)) :
    restrictCube n r (antipode x) = antipode (restrictCube n r x) := by
  rfl

/-- Restricting an edge to the old coordinates gives either an old edge or a
constant pair. This is the precise padding argument in Lemma 2.2. -/
theorem restrictCube_eq_or_adjacent {n r : ℕ} {x y : Cube (n + r)}
    (hxy : CubeAdjacent x y) :
    restrictCube n r x = restrictCube n r y ∨
      CubeAdjacent (restrictCube n r x) (restrictCube n r y) := by
  obtain ⟨k, hk, hrest⟩ := hxy
  by_cases hkn : k.val < n
  · right
    let i : Fin n := ⟨k.val, hkn⟩
    have hik : Fin.castAdd r i = k := Fin.ext rfl
    refine ⟨i, ?_, ?_⟩
    · simpa [restrictCube, hik] using hk
    · intro j hji
      apply hrest
      intro hjk
      apply hji
      apply Fin.ext
      have := congr_arg Fin.val hjk
      simpa [hik] using this
  · left
    funext i
    apply hrest
    intro hik
    have hv := congr_arg Fin.val hik
    simp only [Fin.val_castAdd] at hv
    exact hkn (hv ▸ i.isLt)

/-- The red connected component containing a vertex. -/
def redComponent {n : ℕ} (c : EdgeColoring n) (x : Cube n) :
    (c.colorGraph true).ConnectedComponent :=
  (c.colorGraph true).connectedComponentMk x

theorem redComponent_eq_iff {n : ℕ} (c : EdgeColoring n) (x y : Cube n) :
    redComponent c x = redComponent c y ↔ (c.colorGraph true).Reachable x y :=
  SimpleGraph.ConnectedComponent.eq

theorem redComponent_eq_of_red_edge {n : ℕ} (c : EdgeColoring n) {x y : Cube n}
    (hxy : CubeAdjacent x y) (hred : c x y = true) :
    redComponent c x = redComponent c y :=
  SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj ⟨hxy, hred⟩

/-- The number of red connected components. -/
def redComponentCount {n : ℕ} (c : EdgeColoring n) : ℕ :=
  Fintype.card (c.colorGraph true).ConnectedComponent

/-- Enumerate the red components by `Fin r`. -/
def redComponentIndex {n : ℕ} (c : EdgeColoring n) (x : Cube n) :
    Fin (redComponentCount c) :=
  Fintype.equivFin _ (redComponent c x)

theorem redComponentIndex_injective_on_components {n : ℕ} (c : EdgeColoring n)
    {x y : Cube n} :
    redComponentIndex c x = redComponentIndex c y ↔ redComponent c x = redComponent c y :=
  (Fintype.equivFin _).injective.eq_iff

/-- The label `(p(x),p(Ax))` from Lemma 2.2, padded to a square label set and
to a cube of the same dimension. -/
def counterexampleRookLabeling {n : ℕ} (c : EdgeColoring n) (hc : c.IsAntipodal)
    (hcounter : ¬HasMonochromaticAntipodalPath c) :
    RookLabeling (n + redComponentCount c) (n + redComponentCount c) where
  fst x := Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x))
  snd x := Fin.natAdd n
    (redComponentIndex c (antipode (restrictCube n (redComponentCount c) x)))
  offDiagonal := by
    intro x h
    apply hcounter
    refine ⟨restrictCube n (redComponentCount c) x, true, ?_⟩
    unfold EdgeColoring.MonoConnected
    rw [← redComponent_eq_iff]
    apply (redComponentIndex_injective_on_components c).mp
    exact Fin.natAdd_injective _ n h
  antipodal_fst := by
    intro x
    simp only [restrictCube_antipode]
  antipodal_snd := by
    intro x
    simp only [restrictCube_antipode, antipode_antipode]
  rook := by
    intro x y hxy
    obtain hproj | hproj := restrictCube_eq_or_adjacent hxy
    · left
      rw [hproj]
    · by_cases hred : c (restrictCube n (redComponentCount c) x)
          (restrictCube n (redComponentCount c) y) = true
      · left
        apply congrArg (Fin.natAdd n)
        apply (redComponentIndex_injective_on_components c).mpr
        exact redComponent_eq_of_red_edge c hproj hred
      · right
        apply congrArg (Fin.natAdd n)
        apply (redComponentIndex_injective_on_components c).mpr
        apply redComponent_eq_of_red_edge c
        · exact cubeAdjacent_antipode.mpr hproj
        · rw [hc hproj]
          simpa using hred

/-- The diagonal rook theorem (Theorem 2.3), isolated as the exact combinatorial
statement needed after the reduction. -/
def DiagonalRookTheorem : Prop :=
  ∀ K : ℕ, 2 ≤ K → IsEmpty (RookLabeling K K)

/-- Lemma 2.2 and the deduction following Theorem 2.3, formalized without any
topological assumptions. -/
theorem norine_of_diagonal_rook (hrook : DiagonalRookTheorem) : NorineConjecture := by
  intro n hn c hc
  by_contra hcounter
  let q := counterexampleRookLabeling c hc hcounter
  have hdim : 2 ≤ n + redComponentCount c := by omega
  exact (hrook _ hdim).false q

end

end Norine