theorem
proved
cost_ne_zero_of_inconsistent
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.CostFromDistinction on GitHub at line 190.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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₂₃]
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