Encyclopedia Foundation Foundation Cost From Distinction Uniqueness On Indep Decomposition

ARTICLE 2 claims 2 theorems

Foundation Cost From Distinction Uniqueness On Indep Decomposition

A machine-checked theorem pins down when a cost function for recognition events is fully determined by its values on a small set of building blocks.

Verify this page

The uniqueness theorem

In the Recognition Science framework, a ledger (a discrete record of events) assigns a cost to every configuration of events. The central question is when that cost is uniquely determined. The theorem uniqueness_on_indep_decomposition answers it: if two cost functions agree on a set of basic configurations, and every other configuration can be built by joining independent ones from that set, then the two functions agree everywhere.

The key idea is independent additivity (cost adds when configurations share no predicates). This axiom gives the cost function quantitative structure. The theorem shows that the cost of any configuration equals the sum of costs of its independent inconsistent components, and that the whole function is pinned down by its values on those indecomposable pieces. It is a formal statement in the framework's machine-checked library of formal theorems, derived with zero axioms beyond the standard logical ones.

The theorem does not claim that any particular cost function exists, nor that the set of generators is unique. It only states a conditional: given two cost functions satisfying the axioms, agreement on a generating set forces agreement everywhere. It also does not specify what the cost values are, only that they are determined once the generating values are fixed.

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]
THEOREM additive_strict_of_both_inconsistent · additive_three · IndisputableMonolith/Foundation/CostFromDistinction.lean
additive_strict_of_both_inconsistent · IndisputableMonolith/Foundation/CostFromDistinction.lean:213 
/-- 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
additive_three · IndisputableMonolith/Foundation/CostFromDistinction.lean:197 
/-- Cost is additive over three pairwise-independent configurations.
This is the building block for finite induction. The pairwise
hypotheses `_h₁₂`, `_h₁₃` are stated for readability but only the
joint independence `h₁_join` and the pair-independence `h₂₃` are used
in the proof, since the pairwise structure is encoded in the join. -/
theorem additive_three (κ : CostFunction Config)
    (Γ₁ Γ₂ Γ₃ : Config)
    (_h₁₂ : Independent Γ₁ Γ₂)
    (_h₁₃ : Independent Γ₁ Γ₃)
    (h₂₃ : Independent Γ₂ Γ₃)
    (h₁_join : Independent Γ₁ (join Γ₂ Γ₃)) :
    κ.C (join Γ₁ (join Γ₂ Γ₃)) = κ.C Γ₁ + κ.C Γ₂ + κ.C Γ₃ := by
  rw [κ.additivity Γ₁ (join Γ₂ Γ₃) h₁_join,
      κ.additivity Γ₂ Γ₃ h₂₃]
  ring

What this page does not claim

The theorem does not prove that any particular cost function exists. It does not specify the actual cost values, only their dependence on the generating values. It does not claim that the generating set is unique or canonically chosen.

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