IndisputableMonolith.Foundation.PrimitiveDistinction
IndisputableMonolith/Foundation/PrimitiveDistinction.lean · 333 lines · 15 declarations
show as:
view math explainer →
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.
152-/
153
154/-- The Aristotelian condition (L4) **Composition Consistency** in
155abstract form: there exists a combiner `P` such that the cost of any
156composite operation is determined by the costs of its components,
157with the components combined under the carrier's algebraic structure.
158Specialised to `(ℝ_{>0}, ·)`: -/
159def CompositionConsistency (C : ℝ → ℝ → ℝ) : Prop :=
160 ∃ P : ℝ → ℝ → ℝ,
161 ∀ x y : ℝ, 0 < x → 0 < y →
162 C (x * y) 1 + C (x / y) 1 = P (C x 1) (C y 1)
163
164/-- The equality-induced cost on `ℝ`, taken with the multiplicative
165identity `1` as base point. -/
166noncomputable def hammingCostOnReal (weight : ℝ) : ℝ → ℝ → ℝ :=
167 equalityCost ℝ weight
168
169/-- **The substantive content of (L4).** The equality-induced cost on
170`(ℝ_{>0}, ·)` with positive weight does **not** satisfy Composition
171Consistency. This shows that (L4) is not a definitional fact: it is a
172genuine structural condition that imposes non-trivial compatibility
173between the cost and the carrier's multiplicative structure. -/
174theorem composition_consistency_not_definitional (weight : ℝ) (hw : weight ≠ 0) :
175 ¬ CompositionConsistency (hammingCostOnReal weight) := by
176 intro ⟨P, hP⟩
177 -- Take x = 2, y = 2 (so xy = 4 ≠ 1, x/y = 1).
178 -- Then C(4, 1) + C(1, 1) = weight + 0 = weight.
179 -- And P(C(2, 1), C(2, 1)) = P(weight, weight).
180 have hxy_a : (2 : ℝ) * 2 = 4 := by norm_num
181 have hxy_b : (2 : ℝ) / 2 = 1 := by norm_num
182 have h22 : hammingCostOnReal weight (2 * 2) 1 + hammingCostOnReal weight (2 / 2) 1
183 = P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 2 1) :=
184 hP 2 2 (by norm_num) (by norm_num)
185 have h2val : hammingCostOnReal weight 2 1 = weight := by
186 unfold hammingCostOnReal equalityCost
187 simp
188 have h4val : hammingCostOnReal weight 4 1 = weight := by
189 unfold hammingCostOnReal equalityCost
190 simp
191 have h1val : hammingCostOnReal weight 1 1 = 0 := by
192 unfold hammingCostOnReal equalityCost
193 simp
194 have left22 : hammingCostOnReal weight (2 * 2) 1
195 + hammingCostOnReal weight (2 / 2) 1 = weight := by
196 rw [hxy_a, hxy_b, h4val, h1val, add_zero]
197 have right22 : P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 2 1)
198 = P weight weight := by
199 rw [h2val]
200 have hP22 : P weight weight = weight := by
201 rw [← right22, ← h22, left22]
202 -- Now take x = 2, y = 3 (so xy = 6 ≠ 1, x/y = 2/3 ≠ 1).
203 -- C(6, 1) + C(2/3, 1) = weight + weight = 2*weight.
204 -- P(C(2, 1), C(3, 1)) = P(weight, weight) = weight (from above).
205 -- Contradiction: 2*weight ≠ weight when weight ≠ 0.
206 have hxy_c : (2 : ℝ) * 3 = 6 := by norm_num
207 have h23 : hammingCostOnReal weight (2 * 3) 1
208 + hammingCostOnReal weight (2 / 3) 1
209 = P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 3 1) :=
210 hP 2 3 (by norm_num) (by norm_num)
211 have h6val : hammingCostOnReal weight 6 1 = weight := by
212 unfold hammingCostOnReal equalityCost
213 have : (6 : ℝ) ≠ 1 := by norm_num
214 simp [this]
215 have h23val : hammingCostOnReal weight (2/3 : ℝ) 1 = weight := by
216 unfold hammingCostOnReal equalityCost
217 have : (2/3 : ℝ) ≠ 1 := by norm_num
218 simp [this]
219 have h3val : hammingCostOnReal weight 3 1 = weight := by
220 unfold hammingCostOnReal equalityCost
221 have : (3 : ℝ) ≠ 1 := by norm_num
222 simp [this]
223 have left23 : hammingCostOnReal weight (2 * 3) 1
224 + hammingCostOnReal weight (2 / 3) 1 = 2 * weight := by
225 rw [hxy_c, h6val, h23val]
226 ring
227 have right23 : P (hammingCostOnReal weight 2 1) (hammingCostOnReal weight 3 1)
228 = P weight weight := by
229 rw [h2val, h3val]
230 have hP23 : P weight weight = 2 * weight := by
231 rw [← right23, ← h23, left23]
232 -- Combine: weight = 2*weight, so weight = 0, contradicting hw.
233 have : weight = 2 * weight := hP22.symm.trans hP23
234 have : weight = 0 := by linarith
235 exact hw this
236
237/-! ## The Aristotelian Decomposition
238
239The headline result of this module: the four classical Aristotelian
240conditions, when applied to an equality-derived cost on a carrier with
241multiplicative structure, decompose into three definitional facts and
242one substantive structural condition.
243-/
244
245/-- **The Aristotelian Decomposition.** On any carrier with an
246equality-induced cost:
247
248* (L1) Identity is **definitional**, forced by reflexivity of equality.
249* (L2) Non-Contradiction is **definitional**, forced by symmetry of
250 equality.
251* (L3a) Totality is **definitional**, forced by the function type
252 signature.
253* (L4) Composition Consistency is **substantive**, requiring non-trivial
254 compatibility between the cost and the carrier's algebraic structure;
255 it is not derivable from the type signature alone, as witnessed by
256 the failure of the Hamming cost on `(ℝ_{>0}, ·)`.
257
258This decomposition reduces the foundational surface of the rigidity
259theorem from "seven independent axioms" to "four substantive
260structural conditions plus three definitional facts."
261-/
262theorem aristotelian_decomposition (weight : ℝ) (hw : weight ≠ 0) :
263 -- Definitional: L1, L2, L3a hold for the equality-induced cost.
264 (∀ x : ℝ, equalityCost ℝ weight x x = 0) ∧
265 (∀ x y : ℝ, equalityCost ℝ weight x y = equalityCost ℝ weight y x) ∧
266 (∀ x y : ℝ, ∃ c : ℝ, equalityCost ℝ weight x y = c) ∧
267 -- Substantive: L4 fails for the equality-induced cost, demonstrating
268 -- that L4 is not a type-theoretic consequence.
269 ¬ CompositionConsistency (hammingCostOnReal weight) := by
270 refine ⟨?_, ?_, ?_, ?_⟩
271 · exact identity_from_equality ℝ weight
272 · exact non_contradiction_from_equality ℝ weight
273 · exact totality_from_function_type ℝ weight
274 · exact composition_consistency_not_definitional weight hw
275
276/-! ## Bridge to Logic_FE
277
278Here we connect the new framework to the existing
279`SatisfiesLawsOfLogic` predicate. The bridge says: if a comparison
280operator on `ℝ_{>0}` is derived from an equality cost, then it
281automatically satisfies the Identity and Non-Contradiction conditions
282of Logic_FE, and the rigidity theorem of Logic_FE reduces to imposing
283the substantive conditions (Composition Consistency, Continuity, Scale
284Invariance, polynomial closure, Non-Triviality) on the cost.
285-/
286
287open IndisputableMonolith.Foundation.LogicAsFunctionalEquation
288
289/-- **Bridge theorem.** The Identity and Non-Contradiction conditions
290of `SatisfiesLawsOfLogic` are automatic for any equality-induced cost.
291The remaining four conditions of `SatisfiesLawsOfLogic` (excluded
292middle as continuity, scale invariance, route independence, and
293non-triviality) are the substantive structural axioms. -/
294theorem equality_cost_satisfies_definitional
295 (weight : ℝ) :
296 Identity (hammingCostOnReal weight) ∧
297 NonContradiction (hammingCostOnReal weight) := by
298 refine ⟨?_, ?_⟩
299 · intro x _
300 exact identity_from_equality ℝ weight x
301 · intro x y _ _
302 exact non_contradiction_from_equality ℝ weight x y
303
304/-! ## Summary
305
306The four Aristotelian conditions of Logic_FE are not seven independent
307axioms. Three of them (Identity, Non-Contradiction, Totality) are
308definitional facts forced by the type signature of an equality-induced
309cost. Only the fourth (Composition Consistency) is a genuinely
310substantive structural condition.
311
312The rigidity theorem of Logic_FE therefore rests on:
313
314* **One substantive structural condition** (Composition Consistency):
315 the cost respects the carrier's composition.
316* **Three regularity / structural hypotheses** (Continuity, Scale
317 Invariance, Polynomial-degree-2 closure of the combiner): the cost
318 has the analytic regularity required for the d'Alembert classification
319 to apply.
320* **One existence assumption** (Non-Triviality): the cost is not
321 identically zero.
322* **Three definitional facts** (Identity, Non-Contradiction, Totality):
323 forced by the type signature of the equality-induced cost.
324
325This is the deepest structural decomposition of the Aristotelian
326foundations of comparison-based rigidity that the present framework
327admits.
328-/
329
330end PrimitiveDistinction
331end Foundation
332end IndisputableMonolith
333