Foundation Cost From Distinction Additive Strict Of Both Inconsistent

The additivity theorem

In the Recognition Science framework, a ledger (a discrete record of events) assigns a cost to every configuration of facts. A configuration is consistent if it can all be true at once; it is inconsistent if it contains a contradiction. The framework's basic rule is that consistent configurations cost nothing, while inconsistent ones cost a positive amount. The theorem additive_strict_of_both_inconsistent states a simple consequence: if you take two inconsistent configurations that share no predicates, then the cost of joining them is strictly greater than the cost of either one alone.

The proof is short and depends on two earlier facts. First, the cost of a joined configuration equals the sum of the costs of its independent parts. Second, an inconsistent configuration always has positive cost. So if both parts have positive cost, their sum is strictly larger than either summand. The theorem is a formal statement in the machine-checked library of formal theorems; it is derived entirely from the framework's axioms, with no additional assumptions.

This result matters because it gives the cost function genuine quantitative structure. Without it, the framework could only say that inconsistency is costly, not that combining independent inconsistencies is more costly. The theorem is a step toward the larger claim that the cost function is uniquely determined by its behavior on indecomposable inconsistent pieces. That uniqueness is the framework's bridge to the specific cost formula J(x) = (x + 1/x)/2 - 1, which appears elsewhere in the theory.

/-- The (D) and (A) axioms together imply that the cost of an
independent join of two inconsistent configurations is strictly
larger than each individual cost. -/
theorem additive_strict_of_both_inconsistent (κ : CostFunction Config)
    (Γ₁ Γ₂ : Config)
    (h_indep : Independent Γ₁ Γ₂)
    (h₁ : ¬IsConsistent Γ₁) (h₂ : ¬IsConsistent Γ₂) :
    κ.C (join Γ₁ Γ₂) > κ.C Γ₁ ∧ κ.C (join Γ₁ Γ₂) > κ.C Γ₂ := by
  have h_eq : κ.C (join Γ₁ Γ₂) = κ.C Γ₁ + κ.C Γ₂ :=
    κ.additivity Γ₁ Γ₂ h_indep
  have h₁_pos : 0 < κ.C Γ₁ := cost_pos_of_inconsistent κ Γ₁ h₁
  have h₂_pos : 0 < κ.C Γ₂ := cost_pos_of_inconsistent κ Γ₂ h₂
  refine ⟨?_, ?_⟩
  · linarith
  · linarith

/-- Cost is additive over independent join with the empty configuration
(degenerate case of independent additivity). -/
theorem additive_emp_left (κ : CostFunction Config) (Γ : Config) :
    κ.C (join emp Γ) = κ.C Γ := by
  rw [emp_join]

/-- Inconsistent configurations have positive cost. -/
theorem cost_pos_of_inconsistent (κ : CostFunction Config) (Γ : Config)
    (h : ¬IsConsistent Γ) : 0 < κ.C Γ :=
  (cost_pos_iff_inconsistent κ Γ).mpr h

What this page does not claim

The theorem does not say that joining any two inconsistent configurations increases cost, only those that are independent. The theorem does not establish the specific numeric form of the cost function. The theorem does not claim that recognition work is a physical process; it is a formal constraint.

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: