Encyclopedia Foundation Foundation Primitive Distinction Equality Cost Satisfies Definitional Conditions

ARTICLE 3 claims 3 theorems

Foundation Primitive Distinction Equality Cost Satisfies Definitional Conditions

A simple equality test already satisfies three of the four classical laws of thought, but the fourth, composition, is where real structure begins.

Verify this page

The definitional core

The classical laws of thought, often traced to Aristotle, are usually stated as Identity (a thing is itself), Non-Contradiction (a thing cannot both be and not be itself), and Excluded Middle (a thing either is or is not). In the Recognition Science framework, these appear as conditions on a cost, a function that assigns a number to a pair of objects, measuring how much recognition work separates them. The central declaration equality_cost_satisfies_definitional_conditions proves that a cost derived purely from the equality predicate, which assigns 0 to identical pairs and a fixed positive weight to distinct pairs, automatically satisfies three of the four Aristotelian conditions: Identity, Non-Contradiction, and Totality.

The proof is structural, not empirical. Identity holds because comparing a thing with itself yields 0, forced by the reflexivity of equality. Non-Contradiction holds because the cost is symmetric, so the order of comparison does not matter, a consequence of equality's symmetry. Totality holds because the cost is a total function, defined for every ordered pair in the carrier set. These three facts require no further assumptions beyond the existence of an equality predicate on the type. The fourth condition, Composition Consistency, is different. It requires the cost to respect the carrier's algebraic structure, such as multiplication on the positive reals, and the same declaration proves that an equality-derived cost fails this condition when the weight is nonzero.

This decomposition is the headline result. It reduces the foundational surface of the rigidity theorem from seven independent axioms to four substantive structural conditions plus three definitional facts. The equality cost is too weak to serve as the recognition cost used by the analytic forcing chain, because it ignores the multiplicative composition of the carrier. The theorem equality_cost_insufficient_for_recognition states this explicitly: primitive distinction alone cannot support recognition. A cost that supports the later analysis must respect the carrier's composition, and that compatibility is not derivable from equality alone.

What the declaration does not claim is equally important. It does not prove that the equality cost satisfies all four Aristotelian conditions; it proves the opposite for Composition Consistency. It does not establish that the equality cost is a valid recognition cost; it establishes the insufficiency. And it does not derive the full J-cost function, which requires the substantive conditions of Composition Consistency, Continuity, Scale Invariance, and Non-Triviality. The declaration is a negative result about the equality cost's limitations, and a positive result about which conditions are definitional versus substantive.

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 all four Aristotelian conditions. The equality cost is a valid recognition cost for the forcing chain. The full J-cost function is derived from the equality cost alone.

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