130theorem booker_count_via_law : 131 Fintype.card BookerPlotFamily = 7 := by
proof body
Term-mode proof.
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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.