 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
 144research, not a Lean exercise).
 145-/
 146
 147/-- The opponent-color count law at `D = 2`: red-green, blue-yellow,
 148    and the residual luminance/saturation contrast form three
 149    channels = `2 ^ 2 - 1`. The encoding is left abstract; any
 150    bijection between the three opponent channels and
 151    `F2Power 2 \ {0}` validates the law. -/
 152def OpponentColorCountLaw {OpponentChannel : Type} [Fintype OpponentChannel]
 153    (encoding : OpponentChannel → F2Power 2) : Prop :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.