Encyclopedia Foundation Foundation Primitive Distinction Composition Consistency Not Definitional

ARTICLE 3 claims 3 theorems

Foundation Primitive Distinction Composition Consistency Not Definitional

A simple test shows why recognizing objects requires more than just telling them apart.

Verify this page

The substantive condition

In the Recognition Science framework, a ledger (a discrete record of events) assigns a cost (a number measuring how much work a comparison takes) to every pair of objects. The most basic way to build such a cost is from equality alone: comparing an object with itself costs zero, and comparing two different objects costs some fixed positive weight. This is a Hamming-style cost, named after the classical error-detecting code, and it is the simplest possible distinction predicate.

The framework's machine-checked library of formal theorems proves that this equality-based cost automatically satisfies three classical logical conditions. Identity holds: comparing a thing with itself costs zero. Non-contradiction holds: the cost does not depend on which object you name first. Totality holds: the cost is defined for every pair. These three facts are forced by the very definition of equality and the function type, so they are called definitional. They require no additional assumptions about the objects being compared.

The fourth condition, Composition Consistency, is different. It asks that the cost of a combined operation be determined by the costs of its parts, respecting the algebraic structure of the objects. On positive real numbers with multiplication, the condition takes the form C(x*y, 1) + C(x/y, 1) = P(C(x,1), C(y,1)) for some combiner function P. The theorem composition_consistency_not_definitional proves that the equality-based cost fails this condition whenever the weight is nonzero. Raw distinction is too weak to support recognition; the cost must respect how objects compose, and that compatibility cannot be derived from equality alone.

This result is the positive structural lesson of the module. It shows that the framework's later analytic cost function, which does satisfy Composition Consistency, is not optional decoration but a structural necessity. The four Aristotelian conditions decompose into three definitional facts and one substantive condition, reducing the foundational surface of the rigidity theorem from seven independent axioms to four substantive structural conditions plus three definitional facts. What the theorem does not claim is that Composition Consistency is the only substantive condition, or that the equality-based cost is the only possible primitive distinction. It also does not claim that the failure is a defect; it is precisely the gap that the analytic cost layer fills.

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_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

The theorem does not claim that Composition Consistency is the only substantive condition needed for the rigidity theorem. The theorem does not claim that the equality-based cost is the only possible primitive distinction. The theorem does not claim that the failure of Composition Consistency is a defect in the equality-based cost.

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