CountLawCert

formal source

 174    opponent-color channels (at `D = 2`), and the three massive
 175    electroweak bosons (at `D = 2` in the broken-phase basis with γ
 176    as the zero-eigenvalue element). -/
 177structure CountLawCert where
 178  card_law :
 179    ∀ {D : ℕ} {Family : Type} [Fintype Family]
 180      {encoding : Family → F2Power D},
 181      CountLaw D Family encoding → Fintype.card Family = 2 ^ D - 1
 182  no_extra :
 183    ∀ {D : ℕ} {Family : Type} [Fintype Family]
 184      {encoding : Family → F2Power D},
 185      CountLaw D Family encoding →
 186        ∀ v : F2Power D, v ≠ 0 → ∃ x : Family, encoding x = v
 187  booker_instance :
 188    CountLaw 3 BookerPlotFamily plotEncoding
 189  booker_card_via_law :
 190    Fintype.card BookerPlotFamily = 7
 191
 192/-- The master certificate is inhabited. -/
 193def countLawCert : CountLawCert where
 194  card_law := countLaw_implies_card
 195  no_extra := countLaw_implies_no_extra
 196  booker_instance := bookerCountLaw
 197  booker_card_via_law := booker_count_via_law
 198
 199end
 200
 201end TwoToTheDMinusOne
 202end Patterns
 203end IndisputableMonolith