pith. machine review for the scientific record. sign in
theorem proved term proof

cost_pos_iff_inconsistent

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)

 169theorem cost_pos_iff_inconsistent (κ : CostFunction Config) (Γ : Config) :
 170    0 < κ.C Γ ↔ ¬IsConsistent Γ := by

proof body

Term-mode proof.

 171  constructor
 172  · intro h hc
 173    have h0 : κ.C Γ = 0 := (κ.dichotomy Γ).mpr hc
 174    linarith
 175  · intro hi
 176    have hne : κ.C Γ ≠ 0 := fun heq => hi ((κ.dichotomy Γ).mp heq)
 177    exact lt_of_le_of_ne (κ.nonneg Γ) (Ne.symm hne)
 178
 179/-- Consistent configurations have zero cost. -/

used by (2)

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

depends on (5)

Lean names referenced from this declaration's body.