hammingWeight_le

formal source

 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