inconsistent_of_join_indep_right
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.