pith. machine review for the scientific record. sign in
def definition def or abbrev

regulatoryCeilingCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  51def regulatoryCeilingCert : RegulatoryCeilingCert where
  52  peak := choose_8_4

proof body

Definition body.

  53  peak_is_max := choose_8_4_is_max
  54  fits_double_gap := peak_fits_double_gap
  55  exceeds_gap := peak_exceeds_single_gap
  56  total_256 := totalPowerSet
  57
  58end IndisputableMonolith.CrossDomain.RegulatoryCeiling

depends on (7)

Lean names referenced from this declaration's body.