additive_strict_of_both_inconsistent

formal source

 213/-- The (D) and (A) axioms together imply that the cost of an
 214independent join of two inconsistent configurations is strictly
 215larger than each individual cost. -/
 216theorem additive_strict_of_both_inconsistent (κ : CostFunction Config)
 217    (Γ₁ Γ₂ : Config)
 218    (h_indep : Independent Γ₁ Γ₂)
 219    (h₁ : ¬IsConsistent Γ₁) (h₂ : ¬IsConsistent Γ₂) :
 220    κ.C (join Γ₁ Γ₂) > κ.C Γ₁ ∧ κ.C (join Γ₁ Γ₂) > κ.C Γ₂ := by
 221  have h_eq : κ.C (join Γ₁ Γ₂) = κ.C Γ₁ + κ.C Γ₂ :=
 222    κ.additivity Γ₁ Γ₂ h_indep
 223  have h₁_pos : 0 < κ.C Γ₁ := cost_pos_of_inconsistent κ Γ₁ h₁
 224  have h₂_pos : 0 < κ.C Γ₂ := cost_pos_of_inconsistent κ Γ₂ h₂
 225  refine ⟨?_, ?_⟩
 226  · linarith
 227  · linarith
 228
 229/-- Cost is additive over independent join with the empty configuration
 230(degenerate case of independent additivity). -/
 231theorem additive_emp_left (κ : CostFunction Config) (Γ : Config) :
 232    κ.C (join emp Γ) = κ.C Γ := by
 233  rw [emp_join]
 234
 235theorem additive_emp_right (κ : CostFunction Config) (Γ : Config) :
 236    κ.C (join Γ emp) = κ.C Γ := by
 237  rw [join_emp]
 238
 239/-! ### The Recognition-Work Constraint Theorem -/
 240
 241/--
 242**Recognition-Work Constraint Theorem (uniqueness on independent
 243decompositions).**
 244
 245If two cost functions `κ₁` and `κ₂` on the same configuration space
 246agree on a set `S` of configurations, and if a configuration `Γ`