Encyclopedia Foundation Foundation Primitive Distinction Equality Cost Insufficient For Recognition

ARTICLE 3 claims 3 theorems

Foundation Primitive Distinction Equality Cost Insufficient For Recognition

A cost that only checks whether two things are equal can tell same from different, but it cannot tell how much work recognition takes, and a machine-checked proof shows why.

Verify this page

Why equality alone cannot recognize

A recognition cost, a number assigned to the work of telling two things apart, needs more than a yes-or-no answer. The simplest possible cost is the equality test: identical pairs cost zero, distinct pairs cost some fixed positive weight. In the Recognition Science framework, this is called the equality-induced cost, and it has a natural appeal. It is the first thing anyone would write down.

That first guess fails, and the failure is not a matter of taste. The framework's machine-checked library of formal theorems proves a precise statement: the equality-induced cost on the positive real numbers, with any nonzero weight, does not satisfy the composition consistency condition. That condition asks that the cost of a combined operation be determined by the costs of its parts, respecting how the underlying numbers multiply and divide. The equality cost ignores that structure entirely, so the proof shows it cannot serve as the recognition cost the framework's later analysis needs.

The proof decomposes the classical Aristotelian conditions for a comparison cost into two kinds. Three of them, identity, symmetry, and totality, hold automatically for any equality-derived cost, forced by the definition of equality itself. The fourth, composition consistency, is substantive: it requires real compatibility between the cost and the carrier's algebraic structure, and that compatibility is not derivable from equality alone. The theorem's name says it plainly: equality cost is insufficient for recognition.

What the result does not claim is just as important. It does not say equality is useless; it says equality is too weak. It does not prove that no cost can satisfy composition consistency, only that this particular primitive one cannot. And it does not derive the full J-cost function, the framework's central uniqueness result, from this failure. That derivation belongs to a separate layer of the framework, built on top of the substantive conditions this theorem shows are necessary.

THEOREM composition_consistency_not_definitional · equality_cost_insufficient_for_recognition · IndisputableMonolith/Foundation/PrimitiveDistinction.lean
composition_consistency_not_definitional · IndisputableMonolith/Foundation/PrimitiveDistinction.lean:171 
/-- **The substantive content of (L4).** The equality-induced cost on
`(ℝ_{>0}, ·)` with positive weight does **not** satisfy Composition
Consistency. This is the positive structural lesson: raw distinction is
insufficient for recognition. A cost that supports the later RCL/J-cost
analysis must respect the carrier's multiplicative composition, and that
compatibility is not derivable from equality alone. -/
theorem composition_consistency_not_definitional (weight : ℝ) (hw : weight ≠ 0) :
    ¬ CompositionConsistency (hammingCostOnReal weight) := by
  intro ⟨P, hP⟩
  -- Take x = 2, y = 2 (so xy = 4 ≠ 1, x/y = 1).
  -- Then C(4, 1) + C(1, 1) = weight + 0 = weight.
  -- And P(C(2, 1), C(2, 1)) = P(weight, weight).
  have hxy_a : (2 : ℝ) * 2 = 4 := by norm_num
  have hxy_b : (2 : ℝ) / 2 = 1 := by norm_num
  have h22 : hammingCostOnReal weight (2 * 2) 1 + hammingCostOnReal weight (2 / 2) 1
              = P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 2 1) :=
    hP 2 2 (by norm_num) (by norm_num)
  have h2val : hammingCostOnReal weight 2 1 = weight := by
    unfold hammingCostOnReal equalityCost
    simp
  have h4val : hammingCostOnReal weight 4 1 = weight := by
    unfold hammingCostOnReal equalityCost
    simp
  have h1val : hammingCostOnReal weight 1 1 = 0 := by
    unfold hammingCostOnReal equalityCost
    simp
  have left22 : hammingCostOnReal weight (2 * 2) 1
                  + hammingCostOnReal weight (2 / 2) 1 = weight := by
    rw [hxy_a, hxy_b, h4val, h1val, add_zero]
  have right22 : P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 2 1)
                  = P weight weight := by
    rw [h2val]
  have hP22 : P weight weight = weight := by
    rw [← right22, ← h22, left22]
  -- Now take x = 2, y = 3 (so xy = 6 ≠ 1, x/y = 2/3 ≠ 1).
  -- C(6, 1) + C(2/3, 1) = weight + weight = 2*weight.
  -- P(C(2, 1), C(3, 1)) = P(weight, weight) = weight (from above).
  -- Contradiction: 2*weight ≠ weight when weight ≠ 0.
  have hxy_c : (2 : ℝ) * 3 = 6 := by norm_num
  have h23 : hammingCostOnReal weight (2 * 3) 1
              + hammingCostOnReal weight (2 / 3) 1
              = P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 3 1) :=
    hP 2 3 (by norm_num) (by norm_num)
  have h6val : hammingCostOnReal weight 6 1 = weight := by
    unfold hammingCostOnReal equalityCost
    have : (6 : ℝ) ≠ 1 := by norm_num
    simp [this]
  have h23val : hammingCostOnReal weight (2/3 : ℝ) 1 = weight := by
    unfold hammingCostOnReal equalityCost
    have : (2/3 : ℝ) ≠ 1 := by norm_num
    simp [this]
  have h3val : hammingCostOnReal weight 3 1 = weight := by
    unfold hammingCostOnReal equalityCost
    have : (3 : ℝ) ≠ 1 := by norm_num
    simp [this]
  have left23 : hammingCostOnReal weight (2 * 3) 1
                  + hammingCostOnReal weight (2 / 3) 1 = 2 * weight := by
    rw [hxy_c, h6val, h23val]
    ring
  have right23 : P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 3 1)
                  = P weight weight := by
    rw [h2val, h3val]
  have hP23 : P weight weight = 2 * weight := by
    rw [← right23, ← h23, left23]
  -- Combine: weight = 2*weight, so weight = 0, contradicting hw.
  have : weight = 2 * weight := hP22.symm.trans hP23
  have : weight = 0 := by linarith
  exact hw this
equality_cost_insufficient_for_recognition · IndisputableMonolith/Foundation/PrimitiveDistinction.lean:240 
/-- Positive framing of `composition_consistency_not_definitional`: primitive
equality cost is too weak to be the recognition cost used by the analytic
forcing chain. -/
theorem equality_cost_insufficient_for_recognition (weight : ℝ) (hw : weight ≠ 0) :
    ¬ CompositionConsistency (hammingCostOnReal weight) :=
  composition_consistency_not_definitional weight hw
THEOREM equality_cost_satisfies_definitional_conditions · IndisputableMonolith/Foundation/PrimitiveDistinction.lean
equality_cost_satisfies_definitional_conditions · IndisputableMonolith/Foundation/PrimitiveDistinction.lean:131 
/-- **(L1)+(L2)+(L3a) packaged.** The equality-induced cost satisfies
the three definitional Aristotelian conditions (Identity,
Non-Contradiction, Totality) automatically, with no structural
assumption beyond the existence of an equality predicate on `K`. -/
theorem equality_cost_satisfies_definitional_conditions
    (K : Type*) (weight : ℝ) :
    (∀ x : K, equalityCost K weight x x = 0) ∧
    (∀ x y : K, equalityCost K weight x y = equalityCost K weight y x) ∧
    (∀ x y : K, ∃ c : ℝ, equalityCost K weight x y = c) :=
  ⟨identity_from_equality K weight,
   non_contradiction_from_equality K weight,
   totality_from_function_type K weight⟩
THEOREM aristotelian_decomposition · IndisputableMonolith/Foundation/PrimitiveDistinction.lean
aristotelian_decomposition · IndisputableMonolith/Foundation/PrimitiveDistinction.lean:255 
/-- **The Aristotelian Decomposition.** On any carrier with an
equality-induced cost:

* (L1) Identity is **definitional**, forced by reflexivity of equality.
* (L2) Non-Contradiction is **definitional**, forced by symmetry of
  equality.
* (L3a) Totality is **definitional**, forced by the function type
  signature.
* (L4) Composition Consistency is **substantive**, requiring non-trivial
  compatibility between the cost and the carrier's algebraic structure;
  it is not derivable from the type signature alone, as witnessed by
  the failure of the Hamming cost on `(ℝ_{>0}, ·)`.

This decomposition reduces the foundational surface of the rigidity
theorem from "seven independent axioms" to "four substantive
structural conditions plus three definitional facts."
-/
theorem aristotelian_decomposition (weight : ℝ) (hw : weight ≠ 0) :
    -- Definitional: L1, L2, L3a hold for the equality-induced cost.
    (∀ x : ℝ, equalityCost ℝ weight x x = 0) ∧
    (∀ x y : ℝ, equalityCost ℝ weight x y = equalityCost ℝ weight y x) ∧
    (∀ x y : ℝ, ∃ c : ℝ, equalityCost ℝ weight x y = c) ∧
    -- Substantive: L4 fails for the equality-induced cost, demonstrating
    -- that L4 is not a type-theoretic consequence.
    ¬ CompositionConsistency (hammingCostOnReal weight) := by
  refine ⟨?_, ?_, ?_, ?_⟩
  · exact identity_from_equality ℝ weight
  · exact non_contradiction_from_equality ℝ weight
  · exact totality_from_function_type ℝ weight
  · exact equality_cost_insufficient_for_recognition weight hw

What this page does not claim

Equality is useless; the theorem only says it is too weak to be a recognition cost. No cost can satisfy composition consistency; the theorem only shows this particular equality-derived one cannot. The J-cost function is derived from this failure; that derivation belongs to a separate layer of 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/PrimitiveDistinction.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