Foundation Cost From Distinction Cost Pos Iff Inconsistent

The cost of inconsistency

In the Recognition Science framework, a ledger is a discrete record of events, and a configuration is a collection of such events that may or may not be logically consistent. The framework assigns a cost, a non-negative real number, to each configuration. The theorem cost_pos_iff_inconsistent, proved in the machine-checked library of formal theorems, establishes a simple dichotomy: a configuration has positive cost if and only if it is inconsistent. Consistent configurations have cost zero; inconsistent ones have cost strictly greater than zero.

This result is a direct consequence of two axioms. The first, dichotomy, states that zero cost characterizes consistency. The second, independent additivity, states that the cost of joining two independent configurations equals the sum of their costs. The theorem then follows by a short argument: if a configuration is consistent, its cost must be zero; if it is inconsistent, its cost cannot be zero, and since costs are non-negative, it must be positive.

The theorem does not claim that the cost function is unique, nor does it assign a specific numerical value to any configuration. It establishes only the qualitative dichotomy between zero and positive cost. The framework's library also proves that cost is additive over independent unions, and that two cost functions agreeing on a generating set agree on all configurations decomposable as independent joins of generators. These results give the cost function structure, but the foundational theorem itself is about the sign of the cost, not its magnitude.

In plain terms, the theorem says that in this framework, inconsistency is what costs. A consistent set of events is free; an inconsistent one carries a price. This is the first step toward the framework's larger claim that recognition work, the unit cost of performing a single distinction, forces the entire cost framework. But the theorem itself does not establish that larger claim; it only establishes the sign dichotomy.

/-- Cost is positive if and only if the configuration is inconsistent. -/
theorem cost_pos_iff_inconsistent (κ : CostFunction Config) (Γ : Config) :
    0 < κ.C Γ ↔ ¬IsConsistent Γ := by
  constructor
  · intro h hc
    have h0 : κ.C Γ = 0 := (κ.dichotomy Γ).mpr hc
    linarith
  · intro hi
    have hne : κ.C Γ ≠ 0 := fun heq => hi ((κ.dichotomy Γ).mp heq)
    exact lt_of_le_of_ne (κ.nonneg Γ) (Ne.symm hne)

/-- Consistent configurations have zero cost. -/
theorem cost_zero_of_consistent (κ : CostFunction Config) (Γ : Config)
    (h : IsConsistent Γ) : κ.C Γ = 0 :=
  (κ.dichotomy Γ).mpr h

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

What this page does not claim

The theorem does not assign a specific numerical value to any configuration. The theorem does not establish the uniqueness of the cost function. The theorem does not by itself force the full cost framework; that requires the recognition-work 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: