Encyclopedia Foundation Foundation Cost From Distinction

ARTICLE 3 claims 3 theorems

Foundation Cost From Distinction

A cost function that is zero for consistent facts and positive for contradictions, and adds up over independent parts, is uniquely fixed by its values on the simplest contradictions.

Verify this page

Cost from distinction

In Recognition Science, the ledger (a discrete record of events) assigns a cost to every configuration of facts. The foundational idea is that cost measures how much work it takes to recognize a contradiction. The module CostFromDistinction makes this precise with two plain axioms. First, the dichotomy: a configuration has cost zero exactly when it is consistent, and positive cost exactly when it is inconsistent. Second, independent additivity: if two configurations share no predicates, the cost of joining them is the sum of their individual costs. These two rules give cost a real quantitative structure, not just a yes/no label.

The main theorem, recognition_work_constraint_theorem, states that any cost function satisfying these axioms is uniquely determined by its values on the indecomposable inconsistent configurations. In plain language: once you decide what the simplest contradictions cost, the cost of every larger configuration follows by addition. The theorem also guarantees that such a cost function exists, and it is proved with zero axioms beyond the standard logical ones. The empty configuration has cost zero, and a configuration is consistent if and only if its cost is zero.

This result matters because it turns a vague notion of "recognition work" into a forced mathematical constraint. Without independent additivity, the cost function could be arbitrary. With it, the cost of any configuration is the sum of costs of its independent inconsistent parts. The module also defines a calibration structure: a distinguished inconsistent configuration with a chosen positive cost value, which anchors the scale. Two cost functions that agree on a generating set of configurations agree on all independent joins of those generators.

The practical upshot: the framework's cost function is not a free choice. It is pinned down by two structural axioms and a calibration. This is the foundation on which later results, such as the golden ratio and the eight-tick cycle, are built. The module closes the gap between the informal narrative of recognition work and a formal, machine-checked theorem.

THEOREM recognition_work_constraint_theorem · uniqueness_on_indep_decomposition · IndisputableMonolith/Foundation/CostFromDistinction.lean
recognition_work_constraint_theorem · IndisputableMonolith/Foundation/CostFromDistinction.lean:389 
/--
**Recognition-Work Constraint Theorem (formal headline).**

There exists a master certificate of the recognition-work constraint
on any configuration space and any cost function satisfying the two
bridge axioms. The certificate makes the constraint explicit:

1. The empty configuration has zero cost.
2. Cost is positive iff inconsistent.
3. Cost is additive over independent joins.
4. Two cost functions agreeing on a generating set agree on all
   independent decompositions.

This formalises the substantive constraint that the recognition-work
primitive places on the cost function. Without independent
additivity (axiom A), the dichotomy alone (axiom D) is just a binary
stipulation. With both axioms, the cost function is constrained to
factor through the independent-decomposition structure of the
configuration space.
-/
theorem recognition_work_constraint_theorem
    (κ : CostFunction Config) :
    Nonempty (RecognitionWorkConstraintCert Config) :=
  ⟨recognition_work_constraint_cert κ⟩
uniqueness_on_indep_decomposition · IndisputableMonolith/Foundation/CostFromDistinction.lean:241 
/--
**Recognition-Work Constraint Theorem (uniqueness on independent
decompositions).**

If two cost functions `κ₁` and `κ₂` on the same configuration space
agree on a set `S` of configurations, and if a configuration `Γ`
decomposes as the join of two `S`-elements that are independent of
each other, then `κ₁` and `κ₂` agree at `Γ`.

This is the substantive content of the recognition-work primitive:
once cost is constrained to be additive over independent joins, the
cost function is uniquely determined by its restriction to a
generating set of "indecomposable" configurations. Recognition work
is therefore not just a binary stipulation; it forces the cost
function to factor through the independent-decomposition structure of
the configuration space.
-/
theorem uniqueness_on_indep_decomposition
    (κ₁ κ₂ : CostFunction Config)
    (S : Set Config)
    (h_agree : ∀ Γ ∈ S, κ₁.C Γ = κ₂.C Γ) :
    ∀ Γ₁ Γ₂, Γ₁ ∈ S → Γ₂ ∈ S → Independent Γ₁ Γ₂ →
      κ₁.C (join Γ₁ Γ₂) = κ₂.C (join Γ₁ Γ₂) := by
  intro Γ₁ Γ₂ h₁_mem h₂_mem h_indep
  rw [κ₁.additivity Γ₁ Γ₂ h_indep, κ₂.additivity Γ₁ Γ₂ h_indep,
      h_agree Γ₁ h₁_mem, h_agree Γ₂ h₂_mem]
THEOREM emp_cost_zero · cost_pos_iff_inconsistent · IndisputableMonolith/Foundation/CostFromDistinction.lean
emp_cost_zero · IndisputableMonolith/Foundation/CostFromDistinction.lean:163 
/-- The empty configuration has zero cost. -/
theorem emp_cost_zero (κ : CostFunction Config) :
    κ.C emp = 0 :=
  (κ.dichotomy emp).mpr emp_consistent
cost_pos_iff_inconsistent · IndisputableMonolith/Foundation/CostFromDistinction.lean:168 
/-- 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)
THEOREM uniqueness_on_indep_decomposition · IndisputableMonolith/Foundation/CostFromDistinction.lean
uniqueness_on_indep_decomposition · IndisputableMonolith/Foundation/CostFromDistinction.lean:241 
/--
**Recognition-Work Constraint Theorem (uniqueness on independent
decompositions).**

If two cost functions `κ₁` and `κ₂` on the same configuration space
agree on a set `S` of configurations, and if a configuration `Γ`
decomposes as the join of two `S`-elements that are independent of
each other, then `κ₁` and `κ₂` agree at `Γ`.

This is the substantive content of the recognition-work primitive:
once cost is constrained to be additive over independent joins, the
cost function is uniquely determined by its restriction to a
generating set of "indecomposable" configurations. Recognition work
is therefore not just a binary stipulation; it forces the cost
function to factor through the independent-decomposition structure of
the configuration space.
-/
theorem uniqueness_on_indep_decomposition
    (κ₁ κ₂ : CostFunction Config)
    (S : Set Config)
    (h_agree : ∀ Γ ∈ S, κ₁.C Γ = κ₂.C Γ) :
    ∀ Γ₁ Γ₂, Γ₁ ∈ S → Γ₂ ∈ S → Independent Γ₁ Γ₂ →
      κ₁.C (join Γ₁ Γ₂) = κ₂.C (join Γ₁ Γ₂) := by
  intro Γ₁ Γ₂ h₁_mem h₂_mem h_indep
  rw [κ₁.additivity Γ₁ Γ₂ h_indep, κ₂.additivity Γ₁ Γ₂ h_indep,
      h_agree Γ₁ h₁_mem, h_agree Γ₂ h₂_mem]

What this page does not claim

This module does not derive the specific functional form J(x) = (x + 1/x)/2 - 1. It does not prove that any particular physical configuration is inconsistent. It does not establish the physical recognition-to-linking bridge for three dimensions.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND