Encyclopedia Foundation Foundation Primitive Distinction Equality Cost Satisfies Definitional

ARTICLE 3 claims 3 theorems

Foundation Primitive Distinction Equality Cost Satisfies Definitional

A simple cost function built from equality automatically satisfies three classical laws of thought, but the fourth law requires real structure.

Verify this page

The definitional core

A cost, in the Recognition Science framework, is a function that assigns a number to a pair of things: how much work it takes to tell them apart. The simplest possible cost is the equality cost, which charges nothing when the two things are identical and a fixed positive weight when they are different. This is a Hamming-style distance, a concept familiar from coding theory, applied to any type of object.

The declaration equality_cost_satisfies_definitional proves a compact fact about this cost: it automatically satisfies three of the four Aristotelian conditions the framework uses to characterize a valid recognition cost. First, identity holds: comparing a thing with itself costs zero. Second, non-contradiction holds: the cost is symmetric, so comparing x with y costs the same as comparing y with x. Third, totality holds: the cost is defined for every ordered pair, never undefined. These three facts follow directly from the definition of equality itself, with no further assumptions about the type of objects involved.

The fourth Aristotelian condition, composition consistency, is different. It requires the cost of a combined operation to be determined by the costs of its parts, respecting the algebraic structure of the underlying carrier. The same module proves that the equality cost fails this condition on the positive real numbers with multiplication: a nonzero weight makes composition consistency impossible. This is the substantive content. The equality cost is too weak to serve as the recognition cost that the framework's forcing chain depends on.

The result is a decomposition of the framework's foundational surface. The rigidity theorem that forces the unique cost function J(x) = (x + 1/x)/2 - 1 does not rest on seven independent axioms. Three of its conditions are definitional facts, forced by the type signature of an equality-derived cost. The remaining conditions, including composition consistency, are genuine structural hypotheses. This reduces the axiomatic burden and clarifies what the framework actually assumes.

What the declaration does not claim is equally important. It does not prove that the equality cost satisfies composition consistency; it proves the opposite. It does not establish that the equality cost is a valid recognition cost in the full sense. And it does not derive the unique cost function J. The theorem is a boundary marker: it shows how much structure is automatic, and how much must be added.

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 composition_consistency_not_definitional · 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
THEOREM equality_cost_insufficient_for_recognition · IndisputableMonolith/Foundation/PrimitiveDistinction.lean
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

What this page does not claim

The equality cost satisfies composition consistency; the theorem proves it fails. The equality cost is a valid recognition cost in the full sense; the theorem shows it is insufficient. The unique cost function J(x) = (x + 1/x)/2 - 1 is derived here; that is a separate result.

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