Foundation Cost From Distinction Inconsistent Of Join Indep Right

The inconsistency lemma

In the Recognition Science framework, a configuration is a collection of basic distinctions, and a configuration is consistent when its distinctions can all hold at once. The lemma inconsistent_of_join_indep_right states a simple fact: if you take a consistent configuration and join it with an inconsistent one, and the two share no predicates, the result is inconsistent. The proof is immediate from the symmetric lemma for the left side, and it relies only on the formal definition of independence and consistency.

This lemma is a stepping stone in the framework's account of cost. The framework models cost as a non-negative real number assigned to each configuration, with zero cost exactly for consistent configurations and positive cost for inconsistent ones. The lemma ensures that inconsistency is preserved under independent joins, which is what makes the additivity axiom for cost coherent: if a join of independent parts is inconsistent, its cost must be positive, and that positive cost is the sum of the parts' costs.

The lemma does not claim that every join of an inconsistent configuration with anything is inconsistent. It requires the two configurations to be independent, meaning they share no predicates. It also does not say anything about the numerical value of the cost; it is a purely structural statement about consistency, not about the real-valued cost function. The lemma is a theorem in the framework's machine-checked library of formal theorems, with no axioms beyond the standard logical ones.

/-- The right-version of inconsistency preservation under independent
join, derived from the left version by commutativity and symmetry. -/
theorem inconsistent_of_join_indep_right (Γ₁ Γ₂ : Config)
    (h_indep : Independent Γ₁ Γ₂) (h₂ : ¬IsConsistent Γ₂) :
    ¬IsConsistent (join Γ₁ Γ₂) := by
  rw [join_comm]
  exact inconsistent_of_join_indep_left Γ₂ Γ₁ (independent_symm _ _ h_indep) h₂

What this page does not claim

The lemma does not claim that inconsistency is preserved under joins that are not independent. The lemma does not assign any numerical cost value to configurations. The lemma does not by itself establish the full cost framework; it is one structural ingredient.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/CostFromDistinction.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: