cost_pos_iff_inconsistent

formal source

 166  (κ.dichotomy emp).mpr emp_consistent
 167
 168/-- Cost is positive if and only if the configuration is inconsistent. -/
 169theorem cost_pos_iff_inconsistent (κ : CostFunction Config) (Γ : Config) :
 170    0 < κ.C Γ ↔ ¬IsConsistent Γ := by
 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. -/
 180theorem cost_zero_of_consistent (κ : CostFunction Config) (Γ : Config)
 181    (h : IsConsistent Γ) : κ.C Γ = 0 :=
 182  (κ.dichotomy Γ).mpr h
 183
 184/-- Inconsistent configurations have positive cost. -/
 185theorem cost_pos_of_inconsistent (κ : CostFunction Config) (Γ : Config)
 186    (h : ¬IsConsistent Γ) : 0 < κ.C Γ :=
 187  (cost_pos_iff_inconsistent κ Γ).mpr h
 188
 189/-- Inconsistent configurations have nonzero cost. -/
 190theorem cost_ne_zero_of_inconsistent (κ : CostFunction Config) (Γ : Config)
 191    (h : ¬IsConsistent Γ) : κ.C Γ ≠ 0 := by
 192  have := cost_pos_of_inconsistent κ Γ h
 193  linarith
 194
 195/-! ### Three-way and finite-pairwise-independent additivity -/
 196
 197/-- Cost is additive over three pairwise-independent configurations.
 198This is the building block for finite induction. The pairwise
 199hypotheses `_h₁₂`, `_h₁₃` are stated for readability but only the