Foundation Cost From Distinction Cost Zero Of Consistent

The cost of consistency

A configuration is a collection of basic facts or predicates, and a cost function assigns a non-negative real number to each configuration, meant to represent the work needed to recognize it. The theorem cost_zero_of_consistent states a simple consequence of the framework's axioms: if a configuration is consistent, meaning its facts do not contradict one another, then its cost is exactly zero. This is not an assumption added for convenience; it follows from the dichotomy axiom, which says that zero cost and consistency are equivalent properties, and from the requirement that cost never be negative.

The dichotomy axiom is the load-bearing premise. It states that a configuration has zero cost if and only if it is consistent. From that single equivalence, the theorem is immediate: take any consistent configuration, apply the axiom in the direction that consistency implies zero cost, and the result follows. The proof in the machine-checked library of formal theorems is a direct application of this axiom, with no further steps. The companion theorem cost_pos_of_inconsistent completes the picture: a configuration that is not consistent has strictly positive cost, so the two theorems together partition all configurations into zero-cost consistent ones and positive-cost inconsistent ones.

In Recognition Science, this dichotomy is the first quantitative constraint on the cost function. It establishes that the framework's notion of cost has a sharp threshold: consistency is not a matter of degree, and any inconsistency, however small, carries a positive price. This result does not, by itself, determine what the cost of an inconsistent configuration is, nor does it say how costs combine when configurations are joined. Those questions are addressed by other axioms, in particular independent additivity, which states that the cost of joining two configurations that share no predicates is the sum of their individual costs. The dichotomy and additivity together give the cost function its structure, but the dichotomy alone only fixes the zero-cost boundary.

What the theorem does not claim is just as important. It does not say that consistent configurations are free in any physical sense; it says their cost is zero within the framework's definition of cost as recognition work. It does not assign a numerical value to any inconsistent configuration, and it does not say anything about how consistency itself is determined for a given configuration. Those are separate questions, left to the configuration space's own structure and to further axioms.

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

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

/--
A **cost function** on a configuration space, satisfying the two
axioms of the recognition-work bridge:

* **(D) Dichotomy.** Cost is zero if and only if the configuration is
  consistent.
* **(A) Independent additivity.** Cost is additive over the join of
  two configurations that share no predicates.

The non-negativity of cost is a third axiom for technical convenience;
in the abstract setting we cannot derive it from (D) and (A) alone
without restricting to specific concrete configuration spaces.
-/
structure CostFunction (Config : Type u) [ConfigSpace Config] where
  /-- The cost function itself, taking values in the non-negative reals. -/
  C : Config → ℝ
  /-- Cost is non-negative. -/
  nonneg : ∀ Γ, 0 ≤ C Γ
  /-- (D) Dichotomy: zero cost characterises consistency. -/
  dichotomy : ∀ Γ, C Γ = 0 ↔ IsConsistent Γ
  /-- (A) Independent additivity: the recognition-work constraint. -/
  additivity : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ → C (join Γ₁ Γ₂) = C Γ₁ + C Γ₂

What this page does not claim

The theorem does not assign a numerical cost to any inconsistent configuration. The theorem does not say how consistency is determined for a given configuration. The theorem does not imply that consistent configurations are free in any physical sense, only that their recognition cost is zero within the framework.

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: