IndisputableMonolith.Foundation.PrimitiveDistinction

   1/-
   2  PrimitiveDistinction.lean
   3
   4  Below the four Aristotelian conditions: the type-theoretic floor.
   5
   6  The Logic_FE rigidity theorem starts from a comparison operator
   7  C : K × K → Cost satisfying four classical Aristotelian conditions
   8  (Identity, Non-Contradiction, Excluded Middle, Composition Consistency)
   9  plus regularity and structural conditions. We treated those four
  10  conditions as primitive axioms. This module pushes the foundational
  11  floor one layer lower.
  12
  13  We start from the most primitive object: an equality-derived cost.
  14  Given any type with decidable equality, the canonical cost
  15  C(x, y) := indicator(x ≠ y) is a function on pairs whose definitional
  16  content automatically yields three of the four Aristotelian conditions:
  17  Identity (L1), Non-Contradiction (L2), and Totality (L3a). These are
  18  not axioms; they are consequences of the type signature of equality
  19  combined with the definition of cost-as-indicator.
  20
  21  The fourth condition, Composition Consistency (L4), and the regularity
  22  condition Continuity (L3b), and the structural condition Scale
  23  Invariance (B1), remain substantive: they impose non-trivial
  24  compatibility between the cost and the carrier's algebraic structure
  25  and topology, and they are not forced by the equality-derived cost
  26  alone.
  27
  28  The headline of this module:
  29
  30    `aristotelian_decomposition`:
  31      The four classical Aristotelian conditions on an equality-derived
  32      cost decompose into three definitional facts (L1, L2, L3a) plus
  33      one substantive structural condition (L4 + regularity + invariance).
  34
  35  This cuts the foundational surface of Logic_FE from "seven independent
  36  axioms" to "four substantive conditions plus three definitional facts."
  37
  38  References:
  39    - Logic_FE rigidity paper:
  40      Washburn, "A Functional-Equation Encoding of Logical Consistency
  41      on Continuous Positive-Ratio Comparisons," April 2026.
  42    - Universal Forcing paper:
  43      Washburn, "The Universal Forcing Meta-Theorem," April 2026.
  44-/
  45
  46import Mathlib
  47import IndisputableMonolith.Foundation.LogicAsFunctionalEquation
  48
  49namespace IndisputableMonolith
  50namespace Foundation
  51namespace PrimitiveDistinction
  52
  53open Classical
  54
  55/-! ## The Primitive: Distinction Predicate -/
  56
  57/-- A **distinction predicate** on a carrier `K` is a binary predicate
  58that detects whether two elements are distinguishable. The canonical
  59example is the equality test, available on any type. -/
  60def Distinction (K : Type*) : Type _ := K → K → Prop
  61
  62/-- The canonical distinction induced by equality: two elements are
  63distinct iff they are not equal. This is the most primitive distinction
  64on any type and exists for every type without further structure. -/
  65def equalityDistinction (K : Type*) : Distinction K :=
  66  fun x y => x ≠ y
  67
  68/-- Reflexivity of the canonical distinction: an element is not distinct
  69from itself. This is reflexivity of equality, a definitional fact of any
  70type theory. -/
  71theorem equalityDistinction_irrefl (K : Type*) :
  72    ∀ x : K, ¬ equalityDistinction K x x := by
  73  intro x h
  74  exact h rfl
  75
  76/-- Symmetry of the canonical distinction: distinguishability does not
  77depend on argument order. This is symmetry of disequality, derived from
  78the symmetric definition of equality. -/
  79theorem equalityDistinction_symm (K : Type*) :
  80    ∀ x y : K, equalityDistinction K x y ↔ equalityDistinction K y x := by
  81  intro x y
  82  unfold equalityDistinction
  83  exact ⟨fun h heq => h heq.symm, fun h heq => h heq.symm⟩
  84
  85/-! ## The Equality-Induced Cost -/
  86
  87/-- The **canonical cost induced by equality**: assigns 0 to identical
  88pairs and a positive weight to distinct pairs. This is a function on
  89pairs whose form is determined entirely by the equality predicate. -/
  90noncomputable def equalityCost (K : Type*) (weight : ℝ) : K → K → ℝ :=
  91  fun x y => if x = y then 0 else weight
  92
  93/-! ## The Three Definitional Facts
  94
  95The following three theorems show that an equality-induced cost
  96automatically satisfies three of the four Aristotelian conditions
  97without any structural assumption beyond the type signature.
  98-/
  99
 100/-- **(L1) Identity, derived.** The equality-induced cost satisfies
 101`C(x, x) = 0` definitionally. This is not an axiom; it is the
 102definitional content of "comparing a thing with itself takes no work,"
 103forced by reflexivity of equality. -/
 104theorem identity_from_equality (K : Type*) (weight : ℝ) :
 105    ∀ x : K, equalityCost K weight x x = 0 := by
 106  intro x
 107  unfold equalityCost
 108  simp
 109
 110/-- **(L2) Non-Contradiction, derived.** The equality-induced cost is
 111symmetric in its arguments. This follows from the symmetric definition
 112of equality: `x = y` iff `y = x`. -/
 113theorem non_contradiction_from_equality (K : Type*) (weight : ℝ) :
 114    ∀ x y : K, equalityCost K weight x y = equalityCost K weight y x := by
 115  intro x y
 116  unfold equalityCost
 117  by_cases h : x = y
 118  · subst h; rfl
 119  · have hSymm : ¬ y = x := fun heq => h heq.symm
 120    simp [h, hSymm]
 121
 122/-- **(L3a) Totality, derived.** The equality-induced cost is total:
 123it is defined and returns a value for every ordered pair in `K × K`.
 124This follows from the function type signature alone; there are no
 125input pairs on which the cost is undefined. -/
 126theorem totality_from_function_type (K : Type*) (weight : ℝ) :
 127    ∀ x y : K, ∃ c : ℝ, equalityCost K weight x y = c := by
 128  intro x y
 129  exact ⟨equalityCost K weight x y, rfl⟩
 130
 131/-- **(L1)+(L2)+(L3a) packaged.** The equality-induced cost satisfies
 132the three definitional Aristotelian conditions (Identity,
 133Non-Contradiction, Totality) automatically, with no structural
 134assumption beyond the existence of an equality predicate on `K`. -/
 135theorem equality_cost_satisfies_definitional_conditions
 136    (K : Type*) (weight : ℝ) :
 137    (∀ x : K, equalityCost K weight x x = 0) ∧
 138    (∀ x y : K, equalityCost K weight x y = equalityCost K weight y x) ∧
 139    (∀ x y : K, ∃ c : ℝ, equalityCost K weight x y = c) :=
 140  ⟨identity_from_equality K weight,
 141   non_contradiction_from_equality K weight,
 142   totality_from_function_type K weight⟩
 143
 144/-! ## The Substantive Condition: Composition Consistency
 145
 146The fourth Aristotelian condition, Composition Consistency, is not
 147type-theoretic. It requires the cost to be compatible with the
 148carrier's algebraic structure. We make this precise by exhibiting a
 149comparison operator that satisfies the three definitional conditions
 150but fails Composition Consistency, demonstrating that (L4) is
 151genuinely substantive. Equivalently: primitive distinction by itself is
 152too weak to be a recognition cost. The analytic RCL/J-cost layer is
 153structurally required, not optional.
 154-/
 155
 156/-- The Aristotelian condition (L4) **Composition Consistency** in
 157abstract form: there exists a combiner `P` such that the cost of any
 158composite operation is determined by the costs of its components,
 159with the components combined under the carrier's algebraic structure.
 160Specialised to `(ℝ_{>0}, ·)`: -/
 161def CompositionConsistency (C : ℝ → ℝ → ℝ) : Prop :=
 162  ∃ P : ℝ → ℝ → ℝ,
 163    ∀ x y : ℝ, 0 < x → 0 < y →
 164      C (x * y) 1 + C (x / y) 1 = P (C x 1) (C y 1)
 165
 166/-- The equality-induced cost on `ℝ`, taken with the multiplicative
 167identity `1` as base point. -/
 168noncomputable def hammingCostOnReal (weight : ℝ) : ℝ → ℝ → ℝ :=
 169  equalityCost ℝ weight
 170
 171/-- **The substantive content of (L4).** The equality-induced cost on
 172`(ℝ_{>0}, ·)` with positive weight does **not** satisfy Composition
 173Consistency. This is the positive structural lesson: raw distinction is
 174insufficient for recognition. A cost that supports the later RCL/J-cost
 175analysis must respect the carrier's multiplicative composition, and that
 176compatibility is not derivable from equality alone. -/
 177theorem composition_consistency_not_definitional (weight : ℝ) (hw : weight ≠ 0) :
 178    ¬ CompositionConsistency (hammingCostOnReal weight) := by
 179  intro ⟨P, hP⟩
 180  -- Take x = 2, y = 2 (so xy = 4 ≠ 1, x/y = 1).
 181  -- Then C(4, 1) + C(1, 1) = weight + 0 = weight.
 182  -- And P(C(2, 1), C(2, 1)) = P(weight, weight).
 183  have hxy_a : (2 : ℝ) * 2 = 4 := by norm_num
 184  have hxy_b : (2 : ℝ) / 2 = 1 := by norm_num
 185  have h22 : hammingCostOnReal weight (2 * 2) 1 + hammingCostOnReal weight (2 / 2) 1
 186              = P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 2 1) :=
 187    hP 2 2 (by norm_num) (by norm_num)
 188  have h2val : hammingCostOnReal weight 2 1 = weight := by
 189    unfold hammingCostOnReal equalityCost
 190    simp
 191  have h4val : hammingCostOnReal weight 4 1 = weight := by
 192    unfold hammingCostOnReal equalityCost
 193    simp
 194  have h1val : hammingCostOnReal weight 1 1 = 0 := by
 195    unfold hammingCostOnReal equalityCost
 196    simp
 197  have left22 : hammingCostOnReal weight (2 * 2) 1
 198                  + hammingCostOnReal weight (2 / 2) 1 = weight := by
 199    rw [hxy_a, hxy_b, h4val, h1val, add_zero]
 200  have right22 : P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 2 1)
 201                  = P weight weight := by
 202    rw [h2val]
 203  have hP22 : P weight weight = weight := by
 204    rw [← right22, ← h22, left22]
 205  -- Now take x = 2, y = 3 (so xy = 6 ≠ 1, x/y = 2/3 ≠ 1).
 206  -- C(6, 1) + C(2/3, 1) = weight + weight = 2*weight.
 207  -- P(C(2, 1), C(3, 1)) = P(weight, weight) = weight (from above).
 208  -- Contradiction: 2*weight ≠ weight when weight ≠ 0.
 209  have hxy_c : (2 : ℝ) * 3 = 6 := by norm_num
 210  have h23 : hammingCostOnReal weight (2 * 3) 1
 211              + hammingCostOnReal weight (2 / 3) 1
 212              = P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 3 1) :=
 213    hP 2 3 (by norm_num) (by norm_num)
 214  have h6val : hammingCostOnReal weight 6 1 = weight := by
 215    unfold hammingCostOnReal equalityCost
 216    have : (6 : ℝ) ≠ 1 := by norm_num
 217    simp [this]
 218  have h23val : hammingCostOnReal weight (2/3 : ℝ) 1 = weight := by
 219    unfold hammingCostOnReal equalityCost
 220    have : (2/3 : ℝ) ≠ 1 := by norm_num
 221    simp [this]
 222  have h3val : hammingCostOnReal weight 3 1 = weight := by
 223    unfold hammingCostOnReal equalityCost
 224    have : (3 : ℝ) ≠ 1 := by norm_num
 225    simp [this]
 226  have left23 : hammingCostOnReal weight (2 * 3) 1
 227                  + hammingCostOnReal weight (2 / 3) 1 = 2 * weight := by
 228    rw [hxy_c, h6val, h23val]
 229    ring
 230  have right23 : P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 3 1)
 231                  = P weight weight := by
 232    rw [h2val, h3val]
 233  have hP23 : P weight weight = 2 * weight := by
 234    rw [← right23, ← h23, left23]
 235  -- Combine: weight = 2*weight, so weight = 0, contradicting hw.
 236  have : weight = 2 * weight := hP22.symm.trans hP23
 237  have : weight = 0 := by linarith
 238  exact hw this
 239
 240/-- Positive framing of `composition_consistency_not_definitional`: primitive
 241equality cost is too weak to be the recognition cost used by the analytic
 242forcing chain. -/
 243theorem equality_cost_insufficient_for_recognition (weight : ℝ) (hw : weight ≠ 0) :
 244    ¬ CompositionConsistency (hammingCostOnReal weight) :=
 245  composition_consistency_not_definitional weight hw
 246
 247/-! ## The Aristotelian Decomposition
 248
 249The headline result of this module: the four classical Aristotelian
 250conditions, when applied to an equality-derived cost on a carrier with
 251multiplicative structure, decompose into three definitional facts and
 252one substantive structural condition.
 253-/
 254
 255/-- **The Aristotelian Decomposition.** On any carrier with an
 256equality-induced cost:
 257
 258* (L1) Identity is **definitional**, forced by reflexivity of equality.
 259* (L2) Non-Contradiction is **definitional**, forced by symmetry of
 260  equality.
 261* (L3a) Totality is **definitional**, forced by the function type
 262  signature.
 263* (L4) Composition Consistency is **substantive**, requiring non-trivial
 264  compatibility between the cost and the carrier's algebraic structure;
 265  it is not derivable from the type signature alone, as witnessed by
 266  the failure of the Hamming cost on `(ℝ_{>0}, ·)`.
 267
 268This decomposition reduces the foundational surface of the rigidity
 269theorem from "seven independent axioms" to "four substantive
 270structural conditions plus three definitional facts."
 271-/
 272theorem aristotelian_decomposition (weight : ℝ) (hw : weight ≠ 0) :
 273    -- Definitional: L1, L2, L3a hold for the equality-induced cost.
 274    (∀ x : ℝ, equalityCost ℝ weight x x = 0) ∧
 275    (∀ x y : ℝ, equalityCost ℝ weight x y = equalityCost ℝ weight y x) ∧
 276    (∀ x y : ℝ, ∃ c : ℝ, equalityCost ℝ weight x y = c) ∧
 277    -- Substantive: L4 fails for the equality-induced cost, demonstrating
 278    -- that L4 is not a type-theoretic consequence.
 279    ¬ CompositionConsistency (hammingCostOnReal weight) := by
 280  refine ⟨?_, ?_, ?_, ?_⟩
 281  · exact identity_from_equality ℝ weight
 282  · exact non_contradiction_from_equality ℝ weight
 283  · exact totality_from_function_type ℝ weight
 284  · exact equality_cost_insufficient_for_recognition weight hw
 285
 286/-! ## Bridge to Logic_FE
 287
 288Here we connect the new framework to the existing
 289`SatisfiesLawsOfLogic` predicate. The bridge says: if a comparison
 290operator on `ℝ_{>0}` is derived from an equality cost, then it
 291automatically satisfies the Identity and Non-Contradiction conditions
 292of Logic_FE, and the rigidity theorem of Logic_FE reduces to imposing
 293the substantive conditions (Composition Consistency, Continuity, Scale
 294Invariance, polynomial closure, Non-Triviality) on the cost.
 295-/
 296
 297open IndisputableMonolith.Foundation.LogicAsFunctionalEquation
 298
 299/-- **Bridge theorem.** The Identity and Non-Contradiction conditions
 300of `SatisfiesLawsOfLogic` are automatic for any equality-induced cost.
 301The remaining four conditions of `SatisfiesLawsOfLogic` (excluded
 302middle as continuity, scale invariance, route independence, and
 303non-triviality) are the substantive structural axioms. -/
 304theorem equality_cost_satisfies_definitional
 305    (weight : ℝ) :
 306    Identity (hammingCostOnReal weight) ∧
 307    NonContradiction (hammingCostOnReal weight) := by
 308  refine ⟨?_, ?_⟩
 309  · intro x _
 310    exact identity_from_equality ℝ weight x
 311  · intro x y _ _
 312    exact non_contradiction_from_equality ℝ weight x y
 313
 314/-! ## Summary
 315
 316The four Aristotelian conditions of Logic_FE are not seven independent
 317axioms. Three of them (Identity, Non-Contradiction, Totality) are
 318definitional facts forced by the type signature of an equality-induced
 319cost. Only the fourth (Composition Consistency) is a genuinely
 320substantive structural condition.
 321
 322The rigidity theorem of Logic_FE therefore rests on:
 323
 324* **One substantive structural condition** (Composition Consistency):
 325  the cost respects the carrier's composition.
 326* **Three regularity / structural hypotheses** (Continuity, Scale
 327  Invariance, Polynomial-degree-2 closure of the combiner): the cost
 328  has the analytic regularity required for the d'Alembert classification
 329  to apply.
 330* **One existence assumption** (Non-Triviality): the cost is not
 331  identically zero.
 332* **Three definitional facts** (Identity, Non-Contradiction, Totality):
 333  forced by the type signature of the equality-induced cost.
 334
 335This is the deepest structural decomposition of the Aristotelian
 336foundations of comparison-based rigidity that the present framework
 337admits.
 338-/
 339
 340end PrimitiveDistinction
 341end Foundation
 342end IndisputableMonolith
 343