inconsistent_of_join_indep_right
If two configurations are independent and the second is inconsistent then their join is inconsistent. Researchers formalizing the recognition-work bridge cite this when proving that inconsistency propagates through independent components before defining cost functions. The proof is a one-line term reduction that invokes join commutativity followed by the left-hand version after symmetry of independence.
claimLet Config be a type equipped with the ConfigSpace structure (empty configuration emp, binary join, consistency predicate IsConsistent, and symmetric independence relation Independent). If Γ₁ and Γ₂ are independent and Γ₂ is inconsistent, then the join Γ₁ * Γ₂ is inconsistent.
background
ConfigSpace is the typeclass that abstracts configuration spaces: it supplies an empty element emp, a commutative join operation, the predicate IsConsistent (joint satisfiability), and the relation Independent (no shared predicates), with emp independent of every configuration. The module CostFromDistinction uses this structure to impose the recognition-work constraint: cost must be zero precisely on consistent configurations (dichotomy) and additive over independent joins (additivity). The upstream ConfigSpace class encodes the monoid and independence laws that make the present theorem possible.
proof idea
Term-mode proof. The single rewrite replaces the right-hand join by its commutativity instance; the resulting goal is discharged by applying the left-hand lemma inconsistent_of_join_indep_left to the swapped arguments together with the symmetry instance of Independent.
why it matters in Recognition Science
The lemma supplies one half of the pair needed to close the independent-additivity axiom inside the CostFunction definition. It therefore feeds the later results on cost positivity, uniqueness on indecomposable decompositions, and the main recognition_work_constraint_theorem that the module presents as the formal content of the T-1 to T0 bridge. In the Recognition Science setting it guarantees that the cost of an independent union equals the sum of the costs of its inconsistent parts, which is required before any quantitative ladder or phi-tier counting can be attached.
scope and limits
- Does not prove the left-hand version of inconsistency preservation.
- Does not apply to joins of configurations that share predicates.
- Does not derive additivity of cost; it only preserves inconsistency.
- Does not extend the statement to finite or infinite independent families.
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-/