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

choke_universality

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)

 211def choke_universality : ChokePoint := {

proof body

Definition body.

 212  name := "CPM Universality"
 213  status := "scaffold"  -- Labeled scaffold in spec
 214  consequence := "CPM selection is the ONLY selection mechanism"
 215}
 216
 217/-- Choke Point 2: Cost Axiom Bundle -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.