countLaw_implies_card

formal source

  86
  87/-- If `CountLaw` holds for some encoding, then the family has
  88    cardinality exactly `2 ^ D - 1`. -/
  89theorem countLaw_implies_card {D : ℕ} {Family : Type} [Fintype Family]
  90    {encoding : Family → F2Power D} (hL : CountLaw D Family encoding) :
  91    Fintype.card Family = 2 ^ D - 1 := by
  92  have himage : Finset.univ.image encoding =
  93      Finset.univ.filter (fun v : F2Power D => v ≠ 0) := by
  94    apply Finset.Subset.antisymm
  95    · intro v hv
  96      rcases Finset.mem_image.mp hv with ⟨x, _, hx⟩
  97      rw [Finset.mem_filter, ← hx]
  98      exact ⟨Finset.mem_univ _, hL.nonzero x⟩
  99    · intro v hv
 100      rw [Finset.mem_filter] at hv
 101      rcases hL.surjective_on_nonzero v hv.2 with ⟨x, hx⟩
 102      exact Finset.mem_image.mpr ⟨x, Finset.mem_univ _, hx⟩
 103  have hcard : (Finset.univ.image encoding).card = Fintype.card Family := by
 104    rw [Finset.card_image_of_injective _ hL.injective]
 105    rfl
 106  rw [← hcard, himage, F2Power.nonzero_card]
 107
 108/-! ## §3. The universal "no extra family member" theorem -/
 109
 110/-- Universal "no eighth member" theorem: every non-zero vector is
 111    the encoding of some family member. (Just a re-statement of the
 112    surjectivity field, for symmetric naming.) -/
 113theorem countLaw_implies_no_extra {D : ℕ} {Family : Type} [Fintype Family]
 114    {encoding : Family → F2Power D} (hL : CountLaw D Family encoding)
 115    (v : F2Power D) (hv : v ≠ 0) :
 116    ∃ x : Family, encoding x = v :=
 117  hL.surjective_on_nonzero v hv
 118
 119/-! ## §4. Instance: Booker's seven plots are a `CountLaw 3` -/