countLaw_implies_no_extra

formal source

 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` -/
 120
 121/-- The Booker plot families form a `CountLaw 3` instance via
 122    `plotEncoding`. -/
 123theorem bookerCountLaw :
 124    CountLaw 3 BookerPlotFamily plotEncoding where
 125  injective := plotEncoding_injective
 126  nonzero := plotEncoding_image_nonzero
 127  surjective_on_nonzero := no_eighth_plot
 128
 129/-- Corollary: at `D = 3`, the count law gives `2 ^ 3 - 1 = 7`. -/
 130theorem booker_count_via_law :
 131    Fintype.card BookerPlotFamily = 7 := by
 132  have h := countLaw_implies_card bookerCountLaw
 133  -- h : Fintype.card BookerPlotFamily = 2 ^ 3 - 1
 134  norm_num at h
 135  exact h
 136
 137/-! ## §5. Cross-domain witness sketches
 138
 139The instances below are *one-line* templates: each picks a candidate
 140encoding and asserts `CountLaw` if and only if the encoding meets
 141the three predicates. They are stated as definitions of
 142*hypothetical* count-laws: turning them into theorems requires
 143filling in the explicit encoding for each domain (which is open