Encyclopedia Foundation Foundation Primitive Distinction

ARTICLE 3 claims 3 theorems

Foundation Primitive Distinction

Before any theory of cost, a framework needs a way to tell things apart; the primitive distinction is that first step, and it turns out to be too weak alone.

Verify this page

The primitive distinction

A primitive distinction is the most basic way a framework can tell two things apart. In the Recognition Science framework, it is a binary predicate on a carrier set `K`, a function that takes two elements and returns a proposition: distinguishable or not. The canonical example is the equality test, available on any type. Two elements are distinct if and only if they are not equal. This is the ledger, a discrete record of events, at its most minimal: it records only whether two entries are the same or different, nothing more.

From this single predicate, the framework derives three classical logical laws without any further assumptions. Reflexivity of equality forces the identity law: comparing a thing with itself takes no work, so the cost is zero. Symmetry of equality forces non-contradiction: distinguishability does not depend on argument order. The function type signature alone forces totality: the cost is defined for every ordered pair. These three facts are not axioms; they are definitional consequences of the equality predicate itself, and the machine-checked library of formal theorems proves them for any type `K`.

The fourth Aristotelian condition is different. Composition consistency requires the cost to respect the carrier's algebraic structure: the cost of a composite operation must be determined by the costs of its components. This is not type-theoretic. The framework proves this by exhibiting a counterexample: the equality-induced cost on the positive reals with positive weight fails composition consistency. A cost that merely distinguishes equal from unequal pairs cannot support the later analytic forcing chain, because it ignores how elements combine. Raw distinction is insufficient for recognition.

The headline result is the Aristotelian decomposition. The four classical conditions, applied to an equality-derived cost on a carrier with multiplicative structure, split into three definitional facts and one substantive structural condition. This reduces the foundational surface of the rigidity theorem from seven independent axioms to four substantive structural conditions plus three definitional facts. The framework's library shows that the equality-induced cost satisfies the first three automatically, and fails the fourth, demonstrating that the substantive condition is genuinely required, not optional.

What this establishes in plain language: the framework's entire cost theory does not rest on a stack of arbitrary axioms. Three of the classical laws are forced by the mere act of defining a distinction predicate. Only one condition, composition consistency, carries real structural weight, and it is exactly the condition that connects cost to the carrier's algebra. The primitive distinction is the floor, and the floor alone cannot build the tower.

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 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 primitive distinction alone does not force the J-cost function; composition consistency is required. The equality-induced cost on arbitrary carriers is not claimed to satisfy composition consistency. This module does not establish the full forcing chain; it establishes only the definitional floor.

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