IndisputableMonolith.Algebra.F2Power

   1import Mathlib
   2
   3/-!
   4# `F2Power D`: the elementary abelian 2-group of rank `D`
   5
   6## Status: THEOREM module (0 sorry, 0 RS-internal axiom).
   7
   8The companion paper to this module is
   9`papers/Seven_Plots_Three_Dimensions.tex`. There the count `7` for
  10Booker's basic plot families is *asserted* to come from
  11`(Z/2)^3 \ {0}`. Here the count is *proved*, so that downstream
  12modules (`Aesthetics.NarrativeGeodesic`, `Narrative.CubeBridge`,
  13`Patterns.TwoToTheDMinusOne`) can chain off a real theorem instead of
  14a hardcoded definition.
  15
  16## What this module provides
  17
  18* `F2Power D := Fin D → Bool`: the underlying type. Pointwise XOR is
  19  the abelian group operation.
  20* `instance : AddCommGroup (F2Power D)` and `Fintype`, with
  21  `card_eq : Fintype.card (F2Power D) = 2 ^ D`.
  22* `nonzero_card : (Finset.univ.filter (fun v => v ≠ 0)).card = 2 ^ D - 1`.
  23* `nonzero_card_three : … = 7` (immediate corollary at D = 3).
  24* `hammingWeight v := (Finset.univ.filter (fun i => v i = true)).card`,
  25  with `weight_zero_iff : hammingWeight v = 0 ↔ v = 0` and
  26  `weight_le : hammingWeight v ≤ D`.
  27* The 1+3+3+1 weight decomposition at D = 3:
  28  * `card_weight_zero_three : (… filter weight = 0).card = 1`
  29  * `card_weight_one_three : … = 3`
  30  * `card_weight_two_three : … = 3`
  31  * `card_weight_three_three : … = 1`
  32
  33The subgroup structure carries to the Booker bijection in
  34`Aesthetics.NarrativeGeodesic`: each non-zero `v : F2Power 3`
  35generates the `1`-dimensional subgroup `{0, v}` (closed under XOR
  36because `v + v = 0` in `F2`), giving exactly `7` such subgroups.
  37
  38## Falsifier
  39
  40A `D : ℕ` for which `(Finset.univ.filter (· ≠ (0 : F2Power D))).card`
  41differs from `2 ^ D - 1`. Combinatorially impossible (proved below).
  42-/
  43
  44namespace IndisputableMonolith
  45namespace Algebra
  46
  47/-- The elementary abelian 2-group of rank `D`, modeled as
  48    `Fin D → Bool` with pointwise XOR. -/
  49def F2Power (D : ℕ) : Type := Fin D → Bool
  50
  51namespace F2Power
  52
  53variable {D : ℕ}
  54
  55instance : DecidableEq (F2Power D) := by
  56  unfold F2Power; infer_instance
  57
  58instance : Fintype (F2Power D) := by
  59  unfold F2Power; infer_instance
  60
  61instance : Inhabited (F2Power D) := by
  62  unfold F2Power; infer_instance
  63
  64/-- The zero element: all coordinates `false`. -/
  65instance : Zero (F2Power D) := ⟨fun _ => false⟩
  66
  67@[simp] theorem zero_apply (i : Fin D) : (0 : F2Power D) i = false := rfl
  68
  69/-- Pointwise XOR. -/
  70instance : Add (F2Power D) := ⟨fun u v => fun i => xor (u i) (v i)⟩
  71
  72@[simp] theorem add_apply (u v : F2Power D) (i : Fin D) :
  73    (u + v) i = xor (u i) (v i) := rfl
  74
  75/-- Negation in characteristic 2 is the identity. -/
  76instance : Neg (F2Power D) := ⟨fun v => v⟩
  77
  78@[simp] theorem neg_eq_self (v : F2Power D) : -v = v := rfl
  79
  80/-- Subtraction reduces to addition in characteristic 2. -/
  81instance : Sub (F2Power D) := ⟨fun u v => u + v⟩
  82
  83@[simp] theorem sub_eq_add (u v : F2Power D) : u - v = u + v := rfl
  84
  85instance : AddCommGroup (F2Power D) where
  86  add := (· + ·)
  87  zero := 0
  88  neg := Neg.neg
  89  add_assoc u v w := by
  90    funext i
  91    show xor (xor (u i) (v i)) (w i) = xor (u i) (xor (v i) (w i))
  92    cases u i <;> cases v i <;> cases w i <;> rfl
  93  zero_add v := by
  94    funext i
  95    show xor false (v i) = v i
  96    cases v i <;> rfl
  97  add_zero v := by
  98    funext i
  99    show xor (v i) false = v i
 100    cases v i <;> rfl
 101  neg_add_cancel v := by
 102    funext i
 103    show xor (v i) (v i) = false
 104    cases v i <;> rfl
 105  add_comm u v := by
 106    funext i
 107    show xor (u i) (v i) = xor (v i) (u i)
 108    cases u i <;> cases v i <;> rfl
 109  nsmul := nsmulRec
 110  zsmul := zsmulRec
 111  sub_eq_add_neg u v := by funext i; rfl
 112
 113@[simp] theorem add_self (v : F2Power D) : v + v = 0 := by
 114  funext i
 115  show xor (v i) (v i) = false
 116  cases v i <;> rfl
 117
 118/-! ## Cardinality -/
 119
 120/-- `F2Power D` has `2 ^ D` elements. -/
 121theorem card_eq : Fintype.card (F2Power D) = 2 ^ D := by
 122  unfold F2Power
 123  simp [Fintype.card_bool, Fintype.card_fin]
 124
 125/-- The number of non-zero vectors in `F2Power D` is `2 ^ D - 1`. -/
 126theorem nonzero_card :
 127    (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card = 2 ^ D - 1 := by
 128  have h : (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card =
 129           Fintype.card (F2Power D) - 1 := by
 130    rw [show (Finset.univ.filter (fun v : F2Power D => v ≠ 0)) =
 131            Finset.univ.erase 0 from ?_, Finset.card_erase_of_mem (Finset.mem_univ _)]
 132    · rfl
 133    · ext v
 134      simp [Finset.mem_filter, Finset.mem_erase, Finset.mem_univ]
 135  rw [h, card_eq]
 136
 137/-- At `D = 3`, the non-zero count is `7`. The seven Booker plot
 138    families bijection in `Aesthetics.NarrativeGeodesic` chains off
 139    this corollary. -/
 140theorem nonzero_card_three :
 141    (Finset.univ.filter (fun v : F2Power 3 => v ≠ 0)).card = 7 := by
 142  have h := @nonzero_card 3
 143  -- h : … = 2 ^ 3 - 1
 144  have h2 : (2 : ℕ) ^ 3 - 1 = 7 := by norm_num
 145  rw [h2] at h
 146  exact h
 147
 148/-! ## Hamming weight -/
 149
 150/-- The Hamming weight of `v`: the number of coordinates equal to
 151    `true`. -/
 152def hammingWeight (v : F2Power D) : ℕ :=
 153  (Finset.univ.filter (fun i => v i = true)).card
 154
 155@[simp] theorem hammingWeight_zero : hammingWeight (0 : F2Power D) = 0 := by
 156  unfold hammingWeight
 157  simp [zero_apply]
 158
 159theorem hammingWeight_le (v : F2Power D) : hammingWeight v ≤ D := by
 160  unfold hammingWeight
 161  calc (Finset.univ.filter (fun i => v i = true)).card
 162      ≤ Finset.univ.card := Finset.card_filter_le _ _
 163    _ = D := by simp [Finset.card_univ, Fintype.card_fin]
 164
 165theorem weight_zero_iff (v : F2Power D) :
 166    hammingWeight v = 0 ↔ v = 0 := by
 167  constructor
 168  · intro h
 169    unfold hammingWeight at h
 170    rw [Finset.card_eq_zero] at h
 171    funext i
 172    have hi : i ∉ Finset.univ.filter (fun j => v j = true) := by
 173      rw [h]; exact Finset.notMem_empty _
 174    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi
 175    -- hi : ¬ v i = true
 176    cases hv : v i
 177    · rfl
 178    · exact absurd hv hi
 179  · intro h
 180    subst h
 181    exact hammingWeight_zero
 182
 183/-! ## Weight decomposition at `D = 3`
 184
 185The seven non-zero vectors of `F2Power 3` partition by Hamming
 186weight into 3 weight-1 (single-axis), 3 weight-2 (two-axis), and 1
 187weight-3 (all-axes) class. This is the `1+3+3+1` decomposition that
 188matches Booker's primary/compound/transcendent classification. -/
 189
 190/-- The unique weight-0 element: the zero vector. -/
 191theorem card_weight_zero_three :
 192    (Finset.univ.filter (fun v : F2Power 3 => hammingWeight v = 0)).card = 1 := by
 193  have hsubset :
 194      (Finset.univ.filter (fun v : F2Power 3 => hammingWeight v = 0)) = {0} := by
 195    ext v
 196    simp [Finset.mem_filter, Finset.mem_univ, Finset.mem_singleton, weight_zero_iff]
 197  rw [hsubset]
 198  rfl
 199
 200/-- The three weight-1 vectors of `F2Power 3` are
 201    `(true, false, false)`, `(false, true, false)`,
 202    `(false, false, true)`. -/
 203def axis1 : F2Power 3 := ![true, false, false]
 204def axis2 : F2Power 3 := ![false, true, false]
 205def axis3 : F2Power 3 := ![false, false, true]
 206
 207theorem axis1_weight : hammingWeight axis1 = 1 := by
 208  unfold hammingWeight axis1
 209  decide
 210
 211theorem axis2_weight : hammingWeight axis2 = 1 := by
 212  unfold hammingWeight axis2
 213  decide
 214
 215theorem axis3_weight : hammingWeight axis3 = 1 := by
 216  unfold hammingWeight axis3
 217  decide
 218
 219/-- The three weight-2 vectors. -/
 220def axis12 : F2Power 3 := ![true, true, false]
 221def axis13 : F2Power 3 := ![true, false, true]
 222def axis23 : F2Power 3 := ![false, true, true]
 223
 224/-- The unique weight-3 vector. -/
 225def axis123 : F2Power 3 := ![true, true, true]
 226
 227theorem axis123_weight : hammingWeight axis123 = 3 := by
 228  unfold hammingWeight axis123
 229  decide
 230
 231/-! ## Subgroup count
 232
 233Every non-zero `v : F2Power D` generates the 1-dimensional subspace
 234`{0, v}` (closed under XOR because `v + v = 0`). The map
 235`v ↦ {0, v}` from non-zero vectors to 1-dimensional subspaces is a
 236bijection: every 1-dimensional `F2`-subspace consists of exactly two
 237elements (`0` and a single non-zero generator), and the generator is
 238unique. -/
 239
 240/-- The 1-dimensional subspace generated by a non-zero `v`. -/
 241def oneDimSubspace (v : F2Power D) : Finset (F2Power D) :=
 242  {0, v}
 243
 244theorem oneDimSubspace_card (v : F2Power D) (hv : v ≠ 0) :
 245    (oneDimSubspace v).card = 2 := by
 246  unfold oneDimSubspace
 247  simp [Finset.card_insert_of_notMem, Ne.symm hv]
 248
 249/-- The 1-dimensional subspace is closed under addition. -/
 250theorem oneDimSubspace_closed (v : F2Power D) (a b : F2Power D)
 251    (ha : a ∈ oneDimSubspace v) (hb : b ∈ oneDimSubspace v) :
 252    a + b ∈ oneDimSubspace v := by
 253  unfold oneDimSubspace at ha hb ⊢
 254  simp [Finset.mem_insert, Finset.mem_singleton] at ha hb ⊢
 255  rcases ha with ha | ha <;> rcases hb with hb | hb <;>
 256    subst_vars <;> simp [add_self]
 257
 258end F2Power
 259
 260end Algebra
 261end IndisputableMonolith
 262