weight_zero_iff

formal source

 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