 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₂₃]
 211  ring
 212
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.