pith. machine review for the scientific record. sign in
theorem proved term proof

inconsistent_of_join_indep_right

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 122theorem inconsistent_of_join_indep_right (Γ₁ Γ₂ : Config)
 123    (h_indep : Independent Γ₁ Γ₂) (h₂ : ¬IsConsistent Γ₂) :
 124    ¬IsConsistent (join Γ₁ Γ₂) := by

proof body

Term-mode proof.

 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-/

depends on (27)

Lean names referenced from this declaration's body.