plotEncoding_injective

formal source

 149  | .rebirth              => axis123   -- (true, true, true)
 150
 151/-- The encoding is injective: distinct plots map to distinct vectors. -/
 152theorem plotEncoding_injective : Function.Injective plotEncoding := by
 153  intro p q hpq
 154  cases p <;> cases q <;> first | rfl | (exfalso; revert hpq; decide)
 155
 156/-- Every encoded vector is non-zero. -/
 157theorem plotEncoding_image_nonzero (p : BookerPlotFamily) :
 158    plotEncoding p ≠ 0 := by
 159  cases p <;> decide
 160
 161/-- The image of `plotEncoding` is exactly the seven non-zero
 162    vectors of `F2Power 3`. -/
 163theorem plotEncoding_image_eq_nonzero :
 164    Finset.univ.image plotEncoding =
 165      Finset.univ.filter (fun v : F2Power 3 => v ≠ 0) := by
 166  apply Finset.eq_of_subset_of_card_le
 167  · intro v hv
 168    rcases Finset.mem_image.mp hv with ⟨p, _, hp⟩
 169    rw [Finset.mem_filter, ← hp]
 170    exact ⟨Finset.mem_univ _, plotEncoding_image_nonzero p⟩
 171  · rw [F2Power.nonzero_card_three]
 172    have : (Finset.univ.image plotEncoding).card =
 173           Fintype.card BookerPlotFamily := by
 174      rw [Finset.card_image_of_injective _ plotEncoding_injective]
 175      rfl
 176    rw [this, BookerPlotFamily.card_eq_seven]
 177
 178/-! ## §3. The count theorem (replaces the asserted `:= 7`) -/
 179
 180/-- The number of non-trivial 1-dimensional subgroups of
 181    `Q₃ = F2Power 3` is `2 ^ 3 - 1 = 7`. This is the actual count
 182    theorem, chained off `F2Power.nonzero_card_three`. -/