inconsistent_of_join_indep_right

formal source

 119
 120/-- The right-version of inconsistency preservation under independent
 121join, derived from the left version by commutativity and symmetry. -/
 122theorem inconsistent_of_join_indep_right (Γ₁ Γ₂ : Config)
 123    (h_indep : Independent Γ₁ Γ₂) (h₂ : ¬IsConsistent Γ₂) :
 124    ¬IsConsistent (join Γ₁ Γ₂) := by
 125  rw [join_comm]
 126  exact inconsistent_of_join_indep_left Γ₂ Γ₁ (independent_symm _ _ h_indep) h₂
 127
 128end ConfigSpace
 129
 130/-! ## Cost functions with the dichotomy and additivity axioms -/
 131
 132open ConfigSpace
 133
 134/--
 135A **cost function** on a configuration space, satisfying the two
 136axioms of the recognition-work bridge:
 137
 138* **(D) Dichotomy.** Cost is zero if and only if the configuration is
 139  consistent.
 140* **(A) Independent additivity.** Cost is additive over the join of
 141  two configurations that share no predicates.
 142
 143The non-negativity of cost is a third axiom for technical convenience;
 144in the abstract setting we cannot derive it from (D) and (A) alone
 145without restricting to specific concrete configuration spaces.
 146-/
 147structure CostFunction (Config : Type u) [ConfigSpace Config] where
 148  /-- The cost function itself, taking values in the non-negative reals. -/
 149  C : Config → ℝ
 150  /-- Cost is non-negative. -/
 151  nonneg : ∀ Γ, 0 ≤ C Γ
 152  /-- (D) Dichotomy: zero cost characterises consistency. -/