theorem
proved
booker_count_via_law
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Patterns.TwoToTheDMinusOne on GitHub at line 130.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
BookerPlotFamily -
F2Power -
of -
of -
one -
is -
of -
one -
as -
is -
of -
for -
is -
of -
is -
and -
bookerCountLaw -
CountLaw -
countLaw_implies_card -
one -
one
used by
formal source
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 :=
154 CountLaw 2 OpponentChannel encoding
155
156/-- The massive-electroweak-boson count law at `D = 2`: W, Z, H form
157 three massive bosons = `2 ^ 2 - 1`. The photon is the trivial
158 (zero-eigenvalue) element. The encoding is left abstract; any
159 bijection between the three massive bosons and `F2Power 2 \ {0}`
160 validates the law. -/