CountLaw

formal source

  72/-- A `CountLaw D Family encoding` certifies that `encoding` is a
  73    bijection between `Family` and the non-zero vectors of
  74    `F2Power D`. -/
  75structure CountLaw (D : ℕ) (Family : Type) [Fintype Family]
  76    (encoding : Family → F2Power D) : Prop where
  77  /-- The encoding is injective on `Family`. -/
  78  injective : Function.Injective encoding
  79  /-- The encoding image avoids the zero vector. -/
  80  nonzero : ∀ x : Family, encoding x ≠ 0
  81  /-- Every non-zero vector is in the image of `encoding`. -/
  82  surjective_on_nonzero :
  83    ∀ v : F2Power D, v ≠ 0 → ∃ x : Family, encoding x = v
  84
  85/-! ## §2. The universal cardinality theorem -/
  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