cost_zero_of_consistent

formal source

 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
 200joint independence `h₁_join` and the pair-independence `h₂₃` are used
 201in the proof, since the pairwise structure is encoded in the join. -/
 202theorem additive_three (κ : CostFunction Config)
 203    (Γ₁ Γ₂ Γ₃ : Config)
 204    (_h₁₂ : Independent Γ₁ Γ₂)
 205    (_h₁₃ : Independent Γ₁ Γ₃)
 206    (h₂₃ : Independent Γ₂ Γ₃)
 207    (h₁_join : Independent Γ₁ (join Γ₂ Γ₃)) :
 208    κ.C (join Γ₁ (join Γ₂ Γ₃)) = κ.C Γ₁ + κ.C Γ₂ + κ.C Γ₃ := by
 209  rw [κ.additivity Γ₁ (join Γ₂ Γ₃) h₁_join,
 210      κ.additivity Γ₂ Γ₃ h₂₃]