ZMod_chordMatrix_transpose_eq_neg.lean

lemma val_sub_cases {a b : ZMod N} (hab : a ≠ b) :
    (a - b).val = if b.val ≤ a.val then a.val - b.val else N + a.val - b.val := by
  rcases le_or_gt b.val a.val with h | h
  · simp only [h, ite_true, ZMod.val_sub h]
  · simp only [not_le.mpr h, ite_false]
    have hba : b - a ≠ 0 := sub_ne_zero.mpr (Ne.symm hab)
    have hrw : a - b = -(b - a) := by ring
    rw [hrw, ZMod.neg_val, ite_eq_right hba, ZMod.val_sub (le_of_lt h)]
    have hal : a.val < N := ZMod.val_lt _
    omega

def σ (a b k : ZMod N) : ℤ

lemma σ_shift (a b k c : ZMod N) : σ (a + c) (b + c) (k + c) = σ a b k

lemma σ_sub (a b k : ZMod N) : σ a b k = σ 0 (b - a) (k - a)

lemma σ_antisymm_four {x y z w : ZMod N}
    (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w)
    (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) :
    σ x y z - σ x y w + σ z w x - σ z w y = 0

theorem _root_.ZMod.chordMatrix_transpose_eq_neg {m : ℕ} [NeZero m]
    (a b : Fin m → ZMod (2 * m))
    (hdist : Function.Injective (fun p : Fin m × Bool => bif p.2 then a p.1 else b p.1)) :
    let P : Matrix (Fin m) (Fin m) ℤ := fun i j =>
      (if a j ≠ a i ∧ (a j - a i).val < (b i - a i).val then (1 : ℤ) else 0) -
      (if b j ≠ a i ∧ (b j - a i).val < (b i - a i).val then (1 : ℤ) else 0)
    P.transpose = -P := by
  intro P
  have : NeZero (2 * m) := ⟨Nat.mul_ne_zero two_ne_zero (NeZero.ne m)⟩
  have hd : ∀ (p q : Fin m × Bool), p ≠ q →
      (bif p.2 then a p.1 else b p.1) ≠ (bif q.2 then a q.1 else b q.1) :=
    fun p q h heq => h (hdist heq)
  have haa : ∀ i j, i ≠ j → a i ≠ a j := fun i j h =>
    hd (i, true) (j, true) (by simp [h])
  have hab : ∀ i j, a i ≠ b j := fun i j =>
    hd (i, true) (j, false) (by simp)
  have hbb : ∀ i j, i ≠ j → b i ≠ b j := fun i j h =>
    hd (i, false) (j, false) (by simp [h])
  funext i j
  change
    ((if a i ≠ a j ∧ (a i - a j).val < (b j - a j).val then (1 : ℤ) else 0) -
      (if b i ≠ a j ∧ (b i - a j).val < (b j - a j).val then (1 : ℤ) else 0)) =
    -((if a j ≠ a i ∧ (a j - a i).val < (b i - a i).val then (1 : ℤ) else 0) -
      (if b j ≠ a i ∧ (b j - a i).val < (b i - a i).val then (1 : ℤ) else 0))
  by_cases hij : i = j
  · subst hij
    simp only [ne_eq, not_true_eq_false, false_and, ite_false, sub_self,
      lt_irrefl, and_false, neg_zero]
  · have key : σ (a i) (b i) (a j) - σ (a i) (b i) (b j) +
        σ (a j) (b j) (a i) - σ (a j) (b j) (b i) = 0 :=
      σ_antisymm_four (N := 2 * m) (hab i i) (haa i j hij) (hab i j)
        (hab j i).symm (hbb i j hij) (hab j j)
    unfold σ at key
    linarith