join_emp

formal source

 109variable {Config : Type u} [ConfigSpace Config]
 110
 111/-- Empty is the join identity on the right. -/
 112theorem join_emp (Γ : Config) : join Γ emp = Γ := by
 113  rw [join_comm, emp_join]
 114
 115/-- Independence on the right: `emp` is independent of everything from
 116both sides by symmetry. -/
 117theorem independent_emp (Γ : Config) : Independent Γ emp :=
 118  independent_symm emp Γ (emp_independent Γ)
 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