2607.19276v1 / Repro.lean

all files

import Mathlib

/-!
# Reproduction of Wu--Yang, arXiv:2607.19276v1

This file formalizes the paper's central statement, finite checks in small dimensions,
and the abstract chain-level Borsuk--Ulam obstruction (Lemma 3.1).
-/

namespace Norine

/-! ## R1: a faithful statement of the central theorem -/

/-- The vertices of the `n`-dimensional Boolean hypercube. -/
abbrev CubeVertex (n : ℕ) := Fin n → Bool

/-- Coordinatewise antipode on the Boolean hypercube. -/
def antipode {n : ℕ} (x : CubeVertex n) : CubeVertex n := fun i ↦ !x i

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

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

theorem hammingDist_antipode {n : ℕ} (x y : CubeVertex n) :
    hammingDist (antipode x) (antipode y) = hammingDist x y := by
  change hammingDist (fun i ↦ !x i) (fun i ↦ !y i) = hammingDist x y
  exact hammingDist_comp (fun (_ : Fin n) (b : Bool) ↦ !b) (by
    intro i a b h
    cases a <;> cases b <;> simp_all)

/-- The graph `Qₙ`: two Boolean words are adjacent exactly when they differ in one coordinate. -/
def cubeGraph (n : ℕ) : SimpleGraph (CubeVertex n) where
  Adj x y := hammingDist x y = 1
  symm := by
    rw [symm_def]
    intro x y h
    rw [hammingDist_comm]
    exact h
  loopless := by
    rw [irrefl_def]
    intro x
    simp

instance instDecidableCubeAdj (n : ℕ) : DecidableRel (cubeGraph n).Adj := by
  intro x y
  change Decidable (hammingDist x y = 1)
  infer_instance

/-- An (unoriented) edge of `Qₙ`.  Thus an edge-coloring is literally a function on
the edge set, with no irrelevant values on nonedges. -/
abbrev CubeEdge (n : ℕ) := (cubeGraph n).edgeSet

/-- The edge antipodal to `e`, obtained by complementing both endpoints. -/
def antipodalEdge {n : ℕ} (e : CubeEdge n) : CubeEdge n := by
  refine ⟨Sym2.map antipode e.1, ?_⟩
  rcases e with ⟨e, he⟩
  induction e using Sym2.ind with
  | _ x y =>
      change hammingDist (antipode x) (antipode y) = 1
      rw [hammingDist_antipode]
      exact he

/-- A red--blue edge-coloring; the two Boolean values stand for the two colors. -/
abbrev EdgeColoring (n : ℕ) := CubeEdge n → Bool

/-- The paper's antipodality condition: antipodal edges receive opposite colors. -/
def IsAntipodalColoring {n : ℕ} (c : EdgeColoring n) : Prop :=
  ∀ e, c (antipodalEdge e) = !c e

instance instDecidableIsAntipodalColoring {n : ℕ} (c : EdgeColoring n) :
    Decidable (IsAntipodalColoring c) := by
  unfold IsAntipodalColoring
  infer_instance

/-- Adjacency by an edge having the specified color. -/
def ColoredAdj {n : ℕ} (c : EdgeColoring n) (color : Bool)
    (x y : CubeVertex n) : Prop :=
  ∃ h : (cubeGraph n).Adj x y, c ⟨s(x, y), h⟩ = color

instance instDecidableColoredAdj {n : ℕ} (c : EdgeColoring n) (color : Bool) :
    DecidableRel (ColoredAdj c color) := by
  intro x y
  by_cases hxy : (cubeGraph n).Adj x y
  · exact decidable_of_iff (c ⟨s(x, y), hxy⟩ = color) ⟨
      fun hc ↦ ⟨hxy, hc⟩,
      fun ⟨h, hc⟩ ↦ by simpa only [Subsingleton.elim h hxy] using hc⟩
  · exact isFalse fun ⟨h, _⟩ ↦ hxy h

/-- A graph-theoretic path (not merely a walk) all of whose edges have one color. -/
structure MonochromaticPath {n : ℕ} (c : EdgeColoring n) (color : Bool)
    (start finish : CubeVertex n) : Type where
  vertices : List (CubeVertex n)
  start_eq : vertices.head? = some start
  finish_eq : vertices.getLast? = some finish
  nodup : vertices.Nodup
  chain : vertices.IsChain (ColoredAdj c color)

/-- Theorem 1.1 (Norine's conjecture), stated with exactly the paper's vertices,
unoriented edges, antipodal coloring condition, and monochromatic path conclusion. -/
def NorineConjecture : Prop :=
  ∀ n : ℕ, 2 ≤ n → ∀ c : EdgeColoring n, IsAntipodalColoring c →
    ∃ (x : CubeVertex n) (color : Bool),
      Nonempty (MonochromaticPath c color x (antipode x))

/-! ## R2: finite, decidable checks -/

/-- The spanning subgraph consisting of the edges of one chosen color. -/
def coloredGraph {n : ℕ} (c : EdgeColoring n) (color : Bool) :
    SimpleGraph (CubeVertex n) where
  Adj := ColoredAdj c color
  symm := by
    rw [symm_def]
    rintro x y ⟨hxy, hc⟩
    refine ⟨hxy.symm, ?_⟩
    simpa only [Sym2.eq_swap] using hc
  loopless := by
    rw [irrefl_def]
    rintro x ⟨hxx, _⟩
    exact hxx.ne rfl

instance instDecidableColoredGraphAdj {n : ℕ} (c : EdgeColoring n) (color : Bool) :
    DecidableRel (coloredGraph c color).Adj := instDecidableColoredAdj c color

/-- A decidable version of the conclusion, using connectedness in a monochromatic
spanning subgraph.  On a finite graph this is decided by mathlib's bounded path search. -/
def FiniteNorine (n : ℕ) : Prop :=
  ∀ c : EdgeColoring n, IsAntipodalColoring c →
    ∃ (x : CubeVertex n) (color : Bool),
      (coloredGraph c color).Reachable x (antipode x)

instance instDecidableFiniteNorine (n : ℕ) : Decidable (FiniteNorine n) := by
  unfold FiniteNorine
  infer_instance

/-- Reachability in the one-color graph produces an actual nodup monochromatic path,
so the executable formulation does not weaken the paper's conclusion. -/
theorem reachable_gives_monochromaticPath {n : ℕ} {c : EdgeColoring n} {color : Bool}
    {x y : CubeVertex n} (h : (coloredGraph c color).Reachable x y) :
    Nonempty (MonochromaticPath c color x y) := by
  obtain ⟨p, hp⟩ := h.exists_isPath
  refine ⟨⟨p.support, ?_, ?_, hp.support_nodup, p.isChain_adj_support⟩⟩
  · cases p <;> rfl
  · rw [List.getLast?_eq_getLast_of_ne_nil p.support_ne_nil]
    simp

/-- Exhaustive verification of all `2^4` edge-colorings of `Q₂`. -/
theorem finiteNorine_two : FiniteNorine 2 := by native_decide

/-- Exhaustive verification of all `2^12` edge-colorings of `Q₃` (the antipodal
hypothesis leaves `2^6` relevant colorings). -/
theorem finiteNorine_three : FiniteNorine 3 := by native_decide

/-- Sanity checks for the finite search spaces: `Q₂` and `Q₃` have `n 2^(n-1)`
unoriented edges, namely 4 and 12. -/
theorem card_cubeEdge_two : Fintype.card (CubeEdge 2) = 4 := by native_decide

theorem card_cubeEdge_three : Fintype.card (CubeEdge 3) = 12 := by native_decide

/-- The computed `n = 2` case, converted back to the paper's path formulation. -/
theorem norine_two (c : EdgeColoring 2) (hc : IsAntipodalColoring c) :
    ∃ (x : CubeVertex 2) (color : Bool),
      Nonempty (MonochromaticPath c color x (antipode x)) := by
  obtain ⟨x, color, h⟩ := finiteNorine_two c hc
  exact ⟨x, color, reachable_gives_monochromaticPath h⟩

/-- The computed `n = 3` case, converted back to the paper's path formulation. -/
theorem norine_three (c : EdgeColoring 3) (hc : IsAntipodalColoring c) :
    ∃ (x : CubeVertex 3) (color : Bool),
      Nonempty (MonochromaticPath c color x (antipode x)) := by
  obtain ⟨x, color, h⟩ := finiteNorine_three c hc
  exact ⟨x, color, reachable_gives_monochromaticPath h⟩

/-! The paper's finite rook-labeling formulation (Definition 2.1 / Theorem 2.3). -/

/-- `Ω_K = {(a,b) ∈ [K]^2 | a ≠ b}` (using Lean's zero-based `Fin K`). -/
abbrev RookLabel (K : ℕ) := {ab : Fin K × Fin K // ab.1 ≠ ab.2}

/-- The involution `τ(a,b) = (b,a)` on rook labels. -/
def transposeRook {K : ℕ} (a : RookLabel K) : RookLabel K :=
  ⟨(a.1.2, a.1.1), a.2.symm⟩

/-- Definition 2.1: antipodal labels are transposed, and labels across every cube edge
agree in their first coordinate or agree in their second coordinate. -/
def IsRookLabeling {K : ℕ} (q : CubeVertex K → RookLabel K) : Prop :=
  (∀ x, q (antipode x) = transposeRook (q x)) ∧
  (∀ x y, (cubeGraph K).Adj x y →
    (q x).1.1 = (q y).1.1 ∨ (q x).1.2 = (q y).1.2)

instance instDecidableIsRookLabeling {K : ℕ} (q : CubeVertex K → RookLabel K) :
    Decidable (IsRookLabeling q) := by
  unfold IsRookLabeling
  infer_instance

/-- Exhaustive checks of Theorem 2.3 in its first two dimensions. -/
theorem no_rook_labeling_two : ¬ ∃ q : CubeVertex 2 → RookLabel 2, IsRookLabeling q := by
  native_decide

theorem no_rook_labeling_three : ¬ ∃ q : CubeVertex 3 → RookLabel 3, IsRookLabeling q := by
  native_decide

/-! ### Overshoot: the component-labeling core of Lemma 2.2 -/

theorem coloredAdj_antipode {n : ℕ} {c : EdgeColoring n} (hc : IsAntipodalColoring c)
    {color : Bool} {x y : CubeVertex n} (h : ColoredAdj c color x y) :
    ColoredAdj c (!color) (antipode x) (antipode y) := by
  obtain ⟨hxy, hcolor⟩ := h
  have hanti : (cubeGraph n).Adj (antipode x) (antipode y) := by
    change hammingDist (antipode x) (antipode y) = 1
    rw [hammingDist_antipode]
    exact hxy
  refine ⟨hanti, ?_⟩
  let e : CubeEdge n := ⟨s(x, y), hxy⟩
  have hedge : antipodalEdge e = ⟨s(antipode x, antipode y), hanti⟩ := by
    apply Subtype.ext
    rfl
  calc
    c ⟨s(antipode x, antipode y), hanti⟩ = c (antipodalEdge e) := by rw [hedge]
    _ = !c e := hc e
    _ = !color := by rw [hcolor]

/-- Rook labels over an arbitrary component index type. -/
abbrev RookLabelOn (α : Type*) := {ab : α × α // ab.1 ≠ ab.2}

def transposeRookOn {α : Type*} (a : RookLabelOn α) : RookLabelOn α :=
  ⟨(a.1.2, a.1.1), a.2.symm⟩

/-- The substantive first part of Lemma 2.2: if no red component contains a vertex
and its antipode, component pairs give an antipodally symmetric rook labeling. -/
theorem component_rook_labeling {n : ℕ} (c : EdgeColoring n)
    (hc : IsAntipodalColoring c)
    (hnoRed : ∀ x, ¬(coloredGraph c false).Reachable x (antipode x)) :
    ∃ q : CubeVertex n → RookLabelOn (coloredGraph c false).ConnectedComponent,
      (∀ x, q (antipode x) = transposeRookOn (q x)) ∧
      (∀ x y, (cubeGraph n).Adj x y →
        (q x).1.1 = (q y).1.1 ∨ (q x).1.2 = (q y).1.2) := by
  let component := (coloredGraph c false).connectedComponentMk
  let q : CubeVertex n → RookLabelOn (coloredGraph c false).ConnectedComponent := fun x ↦
    ⟨(component x, component (antipode x)), fun heq ↦
      hnoRed x (SimpleGraph.ConnectedComponent.exact heq)⟩
  refine ⟨q, ?_, ?_⟩
  · intro x
    apply Subtype.ext
    simp [q, component, transposeRookOn]
  · intro x y hxy
    let e : CubeEdge n := ⟨s(x, y), hxy⟩
    cases hcolor : c e with
    | false =>
        left
        change component x = component y
        apply SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
        exact ⟨hxy, hcolor⟩
    | true =>
        right
        change component (antipode x) = component (antipode y)
        apply SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
        change ColoredAdj c false (antipode x) (antipode y)
        simpa using coloredAdj_antipode hc (color := true) ⟨hxy, hcolor⟩

/-- Restriction to the first `n` coordinates of a `K`-cube, for `n ≤ K`. -/
def restrictCube {n K : ℕ} (h : n ≤ K) (x : CubeVertex K) : CubeVertex n :=
  fun i ↦ x (Fin.castLE h i)

@[simp] theorem restrictCube_antipode {n K : ℕ} (h : n ≤ K) (x : CubeVertex K) :
    restrictCube h (antipode x) = antipode (restrictCube h x) := rfl

theorem hammingDist_restrictCube_le {n K : ℕ} (h : n ≤ K) (x y : CubeVertex K) :
    hammingDist (restrictCube h x) (restrictCube h y) ≤ hammingDist x y := by
  unfold hammingDist
  apply Finset.card_le_card_of_injOn (Fin.castLE h)
  · intro i hi
    rw [Finset.mem_coe, Finset.mem_filter] at hi ⊢
    exact ⟨Finset.mem_univ _, by simpa [restrictCube] using hi.2⟩
  · intro a ha b hb hab
    exact Fin.castLE_injective h hab

/-- An edge of the large cube either collapses or remains an edge after restriction. -/
theorem restrictCube_eq_or_adj {n K : ℕ} (h : n ≤ K) {x y : CubeVertex K}
    (hxy : (cubeGraph K).Adj x y) :
    restrictCube h x = restrictCube h y ∨
      (cubeGraph n).Adj (restrictCube h x) (restrictCube h y) := by
  by_cases heq : restrictCube h x = restrictCube h y
  · exact Or.inl heq
  · right
    change hammingDist (restrictCube h x) (restrictCube h y) = 1
    have hpos : 0 < hammingDist (restrictCube h x) (restrictCube h y) :=
      hammingDist_pos.mpr heq
    have hle := hammingDist_restrictCube_le h x y
    change hammingDist x y = 1 at hxy
    omega

/-- Injectively relabel an abstract rook label. -/
def mapRookLabelOn {α β : Type*} (f : α → β) (hf : Function.Injective f)
    (a : RookLabelOn α) : RookLabelOn β :=
  ⟨(f a.1.1, f a.1.2), fun heq ↦ a.2 (hf heq)⟩

@[simp] theorem mapRookLabelOn_transpose {α β : Type*} (f : α → β)
    (hf : Function.Injective f) (a : RookLabelOn α) :
    mapRookLabelOn f hf (transposeRookOn a) = transposeRookOn (mapRookLabelOn f hf a) := rfl

/-- Full finite-extension form of Lemma 2.2: enumerate the red components inside `[K]`
and make the label constant in the new cube coordinates. -/
theorem counterexample_gives_rook_labeling {n K : ℕ} (hnK : n ≤ K)
    (c : EdgeColoring n) (hc : IsAntipodalColoring c)
    (hnoRed : ∀ x, ¬(coloredGraph c false).Reachable x (antipode x))
    (hcomponents : Fintype.card (coloredGraph c false).ConnectedComponent ≤ K) :
    ∃ q : CubeVertex K → RookLabel K, IsRookLabeling q := by
  obtain ⟨q0, hanti, hrook⟩ := component_rook_labeling c hc hnoRed
  let enum := Fintype.equivFin (coloredGraph c false).ConnectedComponent
  let embed : Fin (Fintype.card (coloredGraph c false).ConnectedComponent) → Fin K :=
    Fin.castLE hcomponents
  let labelMap := mapRookLabelOn (embed ∘ enum) (Fin.castLE_injective hcomponents |>.comp enum.injective)
  let q : CubeVertex K → RookLabel K := fun x ↦ labelMap (q0 (restrictCube hnK x))
  refine ⟨q, ?_⟩
  constructor
  · intro x
    change labelMap (q0 (restrictCube hnK (antipode x))) =
      transposeRook (labelMap (q0 (restrictCube hnK x)))
    rw [restrictCube_antipode, hanti]
    rfl
  · intro x y hxy
    obtain heq | hadj := restrictCube_eq_or_adj hnK hxy
    · left
      simp [q, heq]
    · obtain hfirst | hsecond := hrook _ _ hadj
      · left
        exact congrArg (embed ∘ enum) hfirst
      · right
        exact congrArg (embed ∘ enum) hsecond

/-- The paper's deduction of Theorem 1.1 from Theorem 2.3, now fully formal: the only
remaining input for the central theorem is the all-dimensional nonexistence of rook labelings. -/
theorem norineConjecture_of_no_rook_labelings
    (hnoRook : ∀ K, 2 ≤ K → ¬ ∃ q : CubeVertex K → RookLabel K, IsRookLabeling q) :
    NorineConjecture := by
  intro n hn c hc
  by_contra hcounterexample
  have hnoRed : ∀ x, ¬(coloredGraph c false).Reachable x (antipode x) := by
    intro x hreach
    apply hcounterexample
    exact ⟨x, false, reachable_gives_monochromaticPath hreach⟩
  let r := Fintype.card (coloredGraph c false).ConnectedComponent
  let K := max n r
  have hnK : n ≤ K := Nat.le_max_left _ _
  have hrK : r ≤ K := Nat.le_max_right _ _
  obtain ⟨q, hq⟩ := counterexample_gives_rook_labeling hnK c hc hnoRed hrK
  exact hnoRook K (hn.trans hnK) ⟨q, hq⟩

end Norine

namespace ChainBU

/-! ## R3: the paper's chain-level Borsuk--Ulam obstruction (Lemma 3.1) -/

abbrev F₂ := ZMod 2

universe u v

variable {X : ℕ → Type u} [∀ i, AddCommGroup (X i)] [∀ i, Module F₂ (X i)]
variable {Y : ℕ → Type v} [∀ i, AddCommGroup (Y i)] [∀ i, Module F₂ (Y i)]

/-- An augmented nonnegatively graded chain complex of `F₂`-vector spaces, equipped
with an augmentation-preserving chain involution.  The differential `d i` goes from
degree `i+1` to degree `i`. -/
structure InvolutiveAugmentedComplex (X : ℕ → Type u)
    [∀ i, AddCommGroup (X i)] [∀ i, Module F₂ (X i)] where
  d : ∀ i, X (i + 1) →ₗ[F₂] X i
  d_sq : ∀ i (x : X (i + 2)), d i (d (i + 1) x) = 0
  ε : X 0 →ₗ[F₂] F₂
  ε_d : ∀ x : X 1, ε (d 0 x) = 0
  T : ∀ i, X i →ₗ[F₂] X i
  T_sq : ∀ i (x : X i), T i (T i x) = x
  T_d : ∀ i (x : X (i + 1)), d i (T (i + 1) x) = T i (d i x)
  ε_T : ∀ x : X 0, ε (T 0 x) = ε x

/-- The norm operator `ν = id + T` used throughout Lemma 3.1. -/
def ν (C : InvolutiveAugmentedComplex X) (i : ℕ) (x : X i) : X i := x + C.T i x

lemma add_self_eq_zero (x : X i) : x + x = 0 := by
  calc
    x + x = (2 : F₂) • x := (two_smul F₂ x).symm
    _ = 0 := by rw [show (2 : F₂) = 0 by decide, zero_smul]

@[simp] lemma ν_zero (C : InvolutiveAugmentedComplex X) (i : ℕ) : ν C i 0 = 0 := by
  simp [ν]

lemma ν_add (C : InvolutiveAugmentedComplex X) (i : ℕ) (x y : X i) :
    ν C i (x + y) = ν C i x + ν C i y := by
  simp only [ν, map_add]
  abel

lemma ν_ν (C : InvolutiveAugmentedComplex X) (i : ℕ) (x : X i) :
    ν C i (ν C i x) = 0 := by
  simp only [ν, map_add, C.T_sq]
  calc
    x + C.T i x + (C.T i x + x) = (x + x) + (C.T i x + C.T i x) := by abel
    _ = 0 := by rw [add_self_eq_zero, add_self_eq_zero, zero_add]

lemma d_ν (C : InvolutiveAugmentedComplex X) (i : ℕ) (x : X (i + 1)) :
    C.d i (ν C (i + 1) x) = ν C i (C.d i x) := by
  simp [ν, C.T_d]

lemma ε_ν (C : InvolutiveAugmentedComplex X) (x : X 0) : C.ε (ν C 0 x) = 0 := by
  simp only [ν, map_add, C.ε_T]
  exact CharTwo.add_self_eq_zero _

/-- An equivariant, augmentation-preserving chain map, exactly as in Section 3. -/
structure EquivariantAugmentedChainMap
    (C : InvolutiveAugmentedComplex X) (D : InvolutiveAugmentedComplex Y) where
  f : ∀ i, X i →ₗ[F₂] Y i
  chain : ∀ i (x : X (i + 1)), D.d i (f (i + 1) x) = f i (C.d i x)
  augmentation : ∀ x : X 0, D.ε (f 0 x) = C.ε x
  equivariant : ∀ i (x : X i), f i (C.T i x) = D.T i (f i x)

lemma map_ν {C : InvolutiveAugmentedComplex X} {D : InvolutiveAugmentedComplex Y}
    (f : EquivariantAugmentedChainMap C D) (i : ℕ) (x : X i) :
    f.f i (ν C i x) = ν D i (f.f i x) := by
  simp [ν, f.equivariant]

/-- Exactness of the source augmented sequence in degree zero. -/
def ExactAtAugmentation (C : InvolutiveAugmentedComplex X) : Prop :=
  ∀ x : X 0, C.ε x = 0 ↔ ∃ y : X 1, C.d 0 y = x

/-- Exactness in source degrees `1,...,d`.  Index `i` here represents degree `i+1`. -/
def ExactInPositiveDegreesThrough (C : InvolutiveAugmentedComplex X) (d : ℕ) : Prop :=
  ∀ i, i < d → ∀ x : X (i + 1), C.d i x = 0 ↔ ∃ y : X (i + 2), C.d (i + 1) y = x

/-- The paper's equality `ker (id+U_i) = im (id+U_i)` through degree `d`. -/
def NormKernelEqRangeThrough (D : InvolutiveAugmentedComplex Y) (d : ℕ) : Prop :=
  ∀ i, i ≤ d → ∀ y : Y i, ν D i y = 0 ↔ ∃ z : Y i, ν D i z = y

/-- The target has no chains above degree `d`. -/
def VanishesAbove (Y : ℕ → Type v) [∀ i, Zero (Y i)] (d : ℕ) : Prop :=
  ∀ i, d < i → ∀ y : Y i, y = 0

/-- A finite source sequence `x₀,...,xₙ` satisfying `d xᵢ₊₁ = ν xᵢ`. -/
structure Tower (C : InvolutiveAugmentedComplex X) (n : ℕ) where
  x : ∀ i : ℕ, X i
  boundary : ∀ i, i < n → C.d i (x (i + 1)) = ν C i (x i)

def Tower.base (C : InvolutiveAugmentedComplex X) (x0 : X 0) : Tower C 0 where
  x := Function.update (fun i ↦ (0 : X i)) 0 x0
  boundary i hi := (Nat.not_lt_zero i hi).elim

def Tower.snoc {C : InvolutiveAugmentedComplex X} {n : ℕ} (t : Tower C n)
    (last : X (n + 1))
    (hlast : C.d n last = ν C n (t.x n)) : Tower C (n + 1) where
  x := Function.update t.x (n + 1) last
  boundary i hi := by
    by_cases hin : i = n
    · subst i
      simpa using hlast
    · have hi_old : i < n := by omega
      have hi_ne : i ≠ n + 1 := by omega
      have hi1_ne : i + 1 ≠ n + 1 := by omega
      simpa [Function.update, hi_ne, hi1_ne, hin] using
        t.boundary i hi_old

/-- The ascending half of the paper's proof: exactness constructs
`x₀,...,x_{d+1}` with `ε x₀ = 1` and `d xᵢ₊₁ = ν xᵢ`. -/
theorem exists_source_tower (C : InvolutiveAugmentedComplex X) (d : ℕ)
    (hε : Function.Surjective C.ε)
    (h0 : ExactAtAugmentation C)
    (hpos : ExactInPositiveDegreesThrough C d) :
    ∃ t : Tower C (d + 1), C.ε (t.x 0) = 1 := by
  obtain ⟨x0, hx0⟩ := hε 1
  have build : ∀ n, n ≤ d + 1 → ∃ t : Tower C n, C.ε (t.x 0) = 1 := by
    intro n hn
    induction n with
    | zero =>
        refine ⟨Tower.base C x0, ?_⟩
        simpa [Tower.base, Function.update] using hx0
    | succ n ih =>
        obtain ⟨t, ht⟩ := ih (by omega)
        have hn : n ≤ d := by omega
        cases n with
        | zero =>
            obtain ⟨last, hlast⟩ := (h0 (ν C 0 (t.x 0))).mp (ε_ν C (t.x 0))
            exact ⟨t.snoc last hlast, by simpa [Tower.snoc, Function.update] using ht⟩
        | succ k =>
            have hcycle : C.d k (ν C (k + 1) (t.x (k + 1))) = 0 := by
              rw [d_ν, t.boundary k (by omega), ν_ν]
            obtain ⟨last, hlast⟩ :=
              (hpos k (by omega) (ν C (k + 1) (t.x (k + 1)))).mp hcycle
            exact ⟨t.snoc last hlast, by
              simpa [Tower.snoc, Function.update] using ht⟩
  exact build (d + 1) le_rfl

/-- The descending half of the paper's proof.  A target sequence satisfying the same
boundary recurrence and vanishing in degree `d+1` must have augmentation zero in degree zero. -/
theorem target_augmentation_zero (D : InvolutiveAugmentedComplex Y) (d : ℕ)
    (hnorm : NormKernelEqRangeThrough D d)
    (y : ∀ i, Y i)
    (hy : ∀ i, i ≤ d → D.d i (y (i + 1)) = ν D i (y i))
    (htop : y (d + 1) = 0) :
    D.ε (y 0) = 0 := by
  have peel : ∀ k, k ≤ d → ∀ zNext : Y (k + 1),
      D.d k (y (k + 1) + ν D (k + 1) zNext) = 0 → D.ε (y 0) = 0 := by
    intro k hk
    induction k with
    | zero =>
        intro zNext hinvariant
        have hνw : ν D 0 (y 0 + D.d 0 zNext) = 0 := by
          calc
            ν D 0 (y 0 + D.d 0 zNext) =
                ν D 0 (y 0) + ν D 0 (D.d 0 zNext) := ν_add D 0 _ _
            _ = D.d 0 (y 1) + D.d 0 (ν D 1 zNext) := by
              rw [hy 0 hk, d_ν]
            _ = D.d 0 (y 1 + ν D 1 zNext) := by rw [map_add]
            _ = 0 := hinvariant
        obtain ⟨z0, hz0⟩ := (hnorm 0 (by omega) (y 0 + D.d 0 zNext)).mp hνw
        have he := congrArg D.ε hz0
        simpa [ε_ν, D.ε_d] using he.symm
    | succ k ih =>
        intro zNext hinvariant
        have hk' : k ≤ d := by omega
        have hνw : ν D (k + 1) (y (k + 1) + D.d (k + 1) zNext) = 0 := by
          calc
            ν D (k + 1) (y (k + 1) + D.d (k + 1) zNext) =
                ν D (k + 1) (y (k + 1)) +
                  ν D (k + 1) (D.d (k + 1) zNext) := ν_add D _ _ _
            _ = D.d (k + 1) (y (k + 2)) +
                  D.d (k + 1) (ν D (k + 2) zNext) := by
              rw [hy (k + 1) hk, d_ν]
            _ = D.d (k + 1) (y (k + 2) + ν D (k + 2) zNext) := by
              rw [map_add]
            _ = 0 := hinvariant
        obtain ⟨zk, hzk⟩ :=
          (hnorm (k + 1) hk (y (k + 1) + D.d (k + 1) zNext)).mp hνw
        apply ih hk' zk
        calc
          D.d k (y (k + 1) + ν D (k + 1) zk) =
              D.d k (y (k + 1) + (y (k + 1) + D.d (k + 1) zNext)) := by
                rw [hzk]
          _ = D.d k (D.d (k + 1) zNext) := by
                congr 1
                rw [← add_assoc, add_self_eq_zero, zero_add]
          _ = 0 := D.d_sq k zNext
  apply peel d le_rfl 0
  simp [htop]

/-- **Lemma 3.1 (chain-level Borsuk--Ulam obstruction).** Under exactly the paper's
surjectivity, exactness, truncation, and norm kernel=image hypotheses, there is no
equivariant augmentation-preserving chain map from `C` to `D`. -/
theorem chainLevelBorsukUlam
    (C : InvolutiveAugmentedComplex X) (D : InvolutiveAugmentedComplex Y) (d : ℕ)
    (hε : Function.Surjective C.ε)
    (h0 : ExactAtAugmentation C)
    (hpos : ExactInPositiveDegreesThrough C d)
    (hvanish : VanishesAbove Y d)
    (hnorm : NormKernelEqRangeThrough D d) :
    ¬ Nonempty (EquivariantAugmentedChainMap C D) := by
  rintro ⟨f⟩
  obtain ⟨t, ht⟩ := exists_source_tower C d hε h0 hpos
  let y : ∀ i, Y i := fun i ↦ f.f i (t.x i)
  have hy : ∀ i, i ≤ d → D.d i (y (i + 1)) = ν D i (y i) := by
    intro i hi
    dsimp only [y]
    rw [f.chain, t.boundary i (by omega), map_ν]
  have htop : y (d + 1) = 0 := hvanish (d + 1) (by omega) _
  have hzero : D.ε (y 0) = 0 := target_augmentation_zero D d hnorm y hy htop
  have hone : D.ε (y 0) = 1 := by
    dsimp only [y]
    exact (f.augmentation (t.x 0)).trans ht
  have : (0 : F₂) = 1 := hzero.symm.trans hone
  norm_num at this

#print axioms chainLevelBorsukUlam

end ChainBU