IndisputableMonolith.Foundation.LogicAsFunctionalEquation
IndisputableMonolith/Foundation/LogicAsFunctionalEquation.lean · 441 lines · 21 declarations
show as:
view math explainer →
1/-
2 LogicAsFunctionalEquation.lean
3
4 DRAFT for the precursor paper "The Law of Logic as Functional Equation:
5 A Logical Formalization of the Recognition Composition Law."
6
7 Intended canonical location:
8 reality/IndisputableMonolith/Foundation/LogicAsFunctionalEquation.lean
9
10 Status:
11 Level 1 of three (translation theorem; takes the d'Alembert Inevitability
12 Theorem and the canonical reciprocal cost uniqueness theorem as published
13 citations and invokes them as black boxes).
14
15 Strategy:
16 1. Define a ComparisonOperator C : ℝ → ℝ → ℝ.
17 2. Encode the four Aristotelian constraints (identity, non-contradiction,
18 excluded middle, route-independence) as Lean predicates on C, with
19 scale-invariance as the bridge from C-level to F-level statements.
20 3. Define the derived cost function F(r) := C(r, 1).
21 4. Prove the four constraints imply the hypotheses of
22 `bilinear_family_forced` (Inevitability.lean) and
23 `law_of_logic_forces_jcost` (FunctionalEquation.lean).
24 5. Conclude the Recognition Composition Law and the canonical reciprocal
25 cost J(x) = ½(x + 1/x) − 1 are the unique functional form and the
26 unique continuous cost compatible with the laws of logic on continuous
27 comparisons of positive ratios.
28
29 Honest caveat (carried in the precursor paper's Discussion):
30 The polynomial restriction on the route-independence combiner is a
31 regularity assumption inherited from the d'Alembert Inevitability Theorem.
32 Level 2 (planned in `Foundation/GeneralizedDAlembert.lean`) will replace
33 polynomiality with continuity using the classical Aczél–Kannappan–Stetkær
34 classification of continuous d'Alembert solutions.
35
36 References:
37 - Washburn, Zlatanović, Allahyarov.
38 "The d'Alembert Inevitability Theorem."
39 Mathematics (MDPI), 2026.
40 Lean module: `IndisputableMonolith.Foundation.DAlembert.Inevitability`.
41 - Washburn, Zlatanović.
42 "Uniqueness of the Canonical Reciprocal Cost."
43 Mathematics 14 (2026), 935.
44 Lean module: `IndisputableMonolith.Cost.FunctionalEquation`.
45-/
46
47import Mathlib
48import IndisputableMonolith.Foundation.DAlembert.Inevitability
49import IndisputableMonolith.Cost.FunctionalEquation
50
51namespace IndisputableMonolith
52namespace Foundation
53namespace LogicAsFunctionalEquation
54
55open Real
56open IndisputableMonolith.Foundation.DAlembert.Inevitability
57
58/-! ## The Comparison Operator -/
59
60/-- A comparison operator on positive reals takes two positive quantities and
61returns a real-valued cost of comparing them. The four Aristotelian
62constraints below are the structural content of comparison being a
63well-posed operation. -/
64abbrev ComparisonOperator := ℝ → ℝ → ℝ
65
66/-- The cost function derived from a comparison operator by fixing the
67second argument at the multiplicative identity. Under scale invariance,
68this is well-defined on the multiplicative group of positive ratios. -/
69@[simp] def derivedCost (C : ComparisonOperator) : ℝ → ℝ :=
70 fun r => C r 1
71
72/-! ## The Four Aristotelian Constraints
73
74We encode the classical laws of logic as structural constraints on a
75comparison operator. The mapping from Aristotle's propositional
76formulations to functional constraints on C is:
77
78 Identity (A = A) ↦ C(x, x) = 0
79 comparison of a thing with itself is trivial
80 Non-contradiction (¬(A ∧ ¬A))↦ C(x, y) = C(y, x)
81 the cost is single-valued under reordering
82 (with scale invariance, this gives reciprocity
83 F(x) = F(1/x))
84 Excluded middle (A ∨ ¬A) ↦ C is continuous and total on its domain
85 every comparison returns a definite value
86 Composition consistency ↦ Route-independence (the d'Alembert form)
87 comparisons assembled forward and backward
88 must compose by a fixed combining rule
89-/
90
91/-- **Identity**: comparing a thing with itself costs zero. The mathematical
92counterpart of the Aristotelian law A = A. -/
93def Identity (C : ComparisonOperator) : Prop :=
94 ∀ x : ℝ, 0 < x → C x x = 0
95
96/-- **Non-contradiction (reciprocal symmetry)**: the cost of comparing x to y
97equals the cost of comparing y to x. The mathematical counterpart of the
98Aristotelian law ¬(A ∧ ¬A): if comparison were not single-valued under
99reordering, the same comparison would simultaneously hold and not hold. -/
100def NonContradiction (C : ComparisonOperator) : Prop :=
101 ∀ x y : ℝ, 0 < x → 0 < y → C x y = C y x
102
103/-- **Excluded middle (totality and continuity)**: every comparison returns a
104definite real value and small perturbations of inputs give small
105perturbations of cost. The mathematical counterpart of the Aristotelian
106law A ∨ ¬A applied to continuous comparisons: there is no "neither" outcome
107on the comparison's domain. -/
108def ExcludedMiddle (C : ComparisonOperator) : Prop :=
109 ContinuousOn (Function.uncurry C) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ))
110
111/-- **Scale invariance**: the cost of a comparison depends only on the
112ratio of the two quantities. This is the structural bridge from a
113two-argument comparison operator to a one-argument cost on positive ratios.
114It is what allows the four laws of logic, which make no reference to absolute
115scale, to be expressed as constraints on the multiplicative group ℝ₊. -/
116def ScaleInvariant (C : ComparisonOperator) : Prop :=
117 ∀ x y lam : ℝ, 0 < x → 0 < y → 0 < lam →
118 C (lam * x) (lam * y) = C x y
119
120/-- **Route-independence (the d'Alembert form)**: the cost of any composite
121comparison, taken in its symmetric forward-and-backward form on positive
122ratios, is a polynomial function of the constituent ratio costs.
123Concretely: assembling a comparison of ratio xy with a comparison of ratio
124x/y (the symmetric forward+backward decomposition) gives a total cost that
125is some fixed polynomial in the costs of the individual ratios x and y.
126The polynomial restriction is the Level-1 regularity assumption; Level 2
127will replace it with continuity. -/
128def RouteIndependence (C : ComparisonOperator) : Prop :=
129 ∃ P : ℝ → ℝ → ℝ,
130 -- P is a polynomial in two variables of degree ≤ 2.
131 (∃ a b c d e f : ℝ, ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2) ∧
132 -- P is symmetric (consequence of non-contradiction at the combiner level).
133 (∀ u v, P u v = P v u) ∧
134 -- The d'Alembert composition law on the derived cost function.
135 (∀ x y : ℝ, 0 < x → 0 < y →
136 derivedCost C (x * y) + derivedCost C (x / y)
137 = P (derivedCost C x) (derivedCost C y))
138
139/-- A comparison operator is **non-trivial** if there exists at least one
140positive ratio with non-zero cost. (Without this assumption the constant zero
141function vacuously satisfies all the constraints.) -/
142def NonTrivial (C : ComparisonOperator) : Prop :=
143 ∃ x : ℝ, 0 < x ∧ derivedCost C x ≠ 0
144
145/-- A comparison operator **satisfies the laws of logic** if all four
146Aristotelian constraints hold, together with scale invariance (the bridge
147from two-argument to one-argument form) and non-triviality (so that the
148derived cost is not vacuously zero). -/
149structure SatisfiesLawsOfLogic (C : ComparisonOperator) : Prop where
150 identity : Identity C
151 non_contradiction : NonContradiction C
152 excluded_middle : ExcludedMiddle C
153 scale_invariant : ScaleInvariant C
154 route_independence : RouteIndependence C
155 non_trivial : NonTrivial C
156
157/-- Public short name for the continuous positive-ratio Law of Logic.
158
159The longer historical name `SatisfiesLawsOfLogic` remains the underlying
160structure used by existing proofs. This alias is the theorem-facing formula:
161a comparison operator satisfies the Law of Logic exactly when it satisfies
162identity, non-contradiction, excluded middle/continuity, scale invariance,
163route independence, and non-triviality. -/
164abbrev LawOfLogic (C : ComparisonOperator) : Prop :=
165 SatisfiesLawsOfLogic C
166
167/-- Expanded formula for the continuous positive-ratio Law of Logic. -/
168theorem lawOfLogic_iff (C : ComparisonOperator) :
169 LawOfLogic C ↔
170 Identity C ∧
171 NonContradiction C ∧
172 ExcludedMiddle C ∧
173 ScaleInvariant C ∧
174 RouteIndependence C ∧
175 NonTrivial C := by
176 constructor
177 · intro h
178 exact ⟨h.identity, h.non_contradiction, h.excluded_middle,
179 h.scale_invariant, h.route_independence, h.non_trivial⟩
180 · rintro ⟨hId, hNC, hEM, hSI, hRI, hNT⟩
181 exact
182 { identity := hId
183 non_contradiction := hNC
184 excluded_middle := hEM
185 scale_invariant := hSI
186 route_independence := hRI
187 non_trivial := hNT }
188
189/-! ## Translation Lemmas
190
191The four Aristotelian constraints, applied to the derived cost function
192F(r) := C(r, 1), produce the hypotheses of the d'Alembert Inevitability
193Theorem.
194-/
195
196/-- **Translation lemma 1 (Identity ⇒ Normalization)**: If a comparison
197operator satisfies Identity, then the derived cost function takes value
198zero at the multiplicative identity. -/
199theorem identity_implies_normalized (C : ComparisonOperator)
200 (hId : Identity C) :
201 IsNormalized (derivedCost C) := by
202 unfold IsNormalized derivedCost
203 exact hId 1 one_pos
204
205/-- **Translation lemma 2 (Non-contradiction + Scale invariance ⇒ Reciprocity)**:
206If a comparison operator is single-valued under argument reordering and
207depends only on ratios, then the derived cost function is invariant under
208inversion of its argument: F(x) = F(1/x).
209
210The chain of equalities:
211 F(x) = C(x, 1) definition of derivedCost
212 = C(1, x) non-contradiction
213 = C(x⁻¹·1, x⁻¹·x) scale invariance (multiply both args by x⁻¹)
214 = C(x⁻¹, 1) simplify (x⁻¹·1 = x⁻¹, x⁻¹·x = 1)
215 = F(x⁻¹) definition of derivedCost
216-/
217theorem non_contradiction_and_scale_imply_reciprocal
218 (C : ComparisonOperator)
219 (hNC : NonContradiction C)
220 (hSI : ScaleInvariant C) :
221 IsSymmetric (derivedCost C) := by
222 intro x hx
223 have hxinv : (0 : ℝ) < x⁻¹ := inv_pos.mpr hx
224 have hx_ne : (x : ℝ) ≠ 0 := ne_of_gt hx
225 -- Step 1: C(x, 1) = C(1, x) by non-contradiction.
226 have h1 : C x 1 = C 1 x := hNC x 1 hx one_pos
227 -- Step 2: scale invariance with x' = 1, y' = x, λ = x⁻¹ gives
228 -- C(x⁻¹·1, x⁻¹·x) = C(1, x), so C(1, x) = C(x⁻¹·1, x⁻¹·x).
229 have h2 : C 1 x = C (x⁻¹ * 1) (x⁻¹ * x) :=
230 (hSI 1 x x⁻¹ one_pos hx hxinv).symm
231 -- Step 3: simplify x⁻¹·1 = x⁻¹ and x⁻¹·x = 1.
232 have h3 : C (x⁻¹ * 1) (x⁻¹ * x) = C x⁻¹ 1 := by
233 rw [mul_one, inv_mul_cancel₀ hx_ne]
234 show derivedCost C x = derivedCost C x⁻¹
235 unfold derivedCost
236 exact h1.trans (h2.trans h3)
237
238/-- **Translation lemma 3 (Excluded middle ⇒ Continuity)**: If a comparison
239operator is jointly continuous in both arguments on the positive quadrant,
240then the derived cost function is continuous on (0, ∞).
241
242The derivedCost C is the composition r ↦ (r, 1) ↦ C(r, 1). The pair-map is
243continuous everywhere; the uncurried C is continuous on the positive
244quadrant by ExcludedMiddle. The pair-map sends (0, ∞) into the positive
245quadrant. Hence the composition is continuous on (0, ∞). -/
246theorem excluded_middle_implies_continuous
247 (C : ComparisonOperator)
248 (hEM : ExcludedMiddle C) :
249 ContinuousOn (derivedCost C) (Set.Ioi 0) := by
250 -- Pair-map r ↦ (r, 1) is continuous everywhere.
251 have h_pair_cont : Continuous (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ)) :=
252 continuous_id.prodMk continuous_const
253 have h_pair_on : ContinuousOn (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
254 (Set.Ioi (0 : ℝ)) :=
255 h_pair_cont.continuousOn
256 -- Pair-map sends (0,∞) into the positive quadrant.
257 have h_maps : Set.MapsTo (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
258 (Set.Ioi (0 : ℝ)) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ)) := by
259 intro s hs
260 refine ⟨?_, ?_⟩
261 · exact hs
262 · show (0 : ℝ) < 1
263 exact one_pos
264 -- Compose to get continuity of (uncurry C) ∘ pair on (0,∞).
265 have h_comp : ContinuousOn
266 ((Function.uncurry C) ∘ fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
267 (Set.Ioi (0 : ℝ)) :=
268 hEM.comp h_pair_on h_maps
269 -- The composition equals derivedCost C definitionally.
270 have h_eq : ((Function.uncurry C) ∘ fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
271 = derivedCost C := by
272 funext s
273 rfl
274 rw [h_eq] at h_comp
275 exact h_comp
276
277/-- **Translation lemma 4 (Route-independence ⇒ Multiplicative consistency
278with a symmetric polynomial combiner)**: extracted directly from the
279definition of `RouteIndependence`. -/
280theorem route_independence_implies_multiplicative_consistency
281 (C : ComparisonOperator)
282 (hRI : RouteIndependence C) :
283 ∃ P : ℝ → ℝ → ℝ,
284 (∃ a b c d e f : ℝ, ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2) ∧
285 (∀ u v, P u v = P v u) ∧
286 HasMultiplicativeConsistency (derivedCost C) P := by
287 obtain ⟨P, hPoly, hSym, hCons⟩ := hRI
288 refine ⟨P, hPoly, hSym, ?_⟩
289 intro x y hx hy
290 exact hCons x y hx hy
291
292/-! ## The Translation Theorem -/
293
294/-- **Translation Theorem**: A comparison operator satisfying the four
295Aristotelian constraints, together with scale invariance and non-triviality,
296satisfies the hypotheses of the d'Alembert Inevitability Theorem on its
297derived cost function.
298
299This is the core technical content of the precursor paper. Once this is in
300hand, the existing peer-reviewed and machine-verified theorems
301(`bilinear_family_forced`, `law_of_logic_forces_jcost`) close the chain. -/
302theorem laws_of_logic_imply_dalembert_hypotheses
303 (C : ComparisonOperator) (hLaws : SatisfiesLawsOfLogic C) :
304 IsNormalized (derivedCost C) ∧
305 IsSymmetric (derivedCost C) ∧
306 (∃ P : ℝ → ℝ → ℝ,
307 (∃ a b c d e f : ℝ, ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2) ∧
308 (∀ u v, P u v = P v u) ∧
309 HasMultiplicativeConsistency (derivedCost C) P) ∧
310 ContinuousOn (derivedCost C) (Set.Ioi 0) ∧
311 (∃ x : ℝ, 0 < x ∧ derivedCost C x ≠ 0) := by
312 refine ⟨?_, ?_, ?_, ?_, ?_⟩
313 · exact identity_implies_normalized C hLaws.identity
314 · exact non_contradiction_and_scale_imply_reciprocal C
315 hLaws.non_contradiction hLaws.scale_invariant
316 · exact route_independence_implies_multiplicative_consistency C
317 hLaws.route_independence
318 · exact excluded_middle_implies_continuous C hLaws.excluded_middle
319 · exact hLaws.non_trivial
320
321/-! ## Main Theorem: RCL is the Unique Functional Form of the Laws of Logic -/
322
323/-- **Main theorem (Logical Formalization Theorem)**: For a comparison
324operator satisfying the four Aristotelian constraints with scale invariance
325and non-triviality, the route-independence combiner is necessarily of the
326Recognition Composition Law form: `P(u,v) = 2u + 2v + c·uv` for some
327constant c ∈ ℝ.
328
329In other words: the unique functional form the laws of logic can take on
330continuous comparisons of positive ratios, under the polynomial regularity
331assumption, is the Recognition Composition Law.
332
333This is an immediate corollary of `laws_of_logic_imply_dalembert_hypotheses`
334combined with `bilinear_family_forced` (Inevitability.lean), which has been
335peer-reviewed in:
336
337 Washburn, Zlatanović, Allahyarov.
338 "The d'Alembert Inevitability Theorem."
339 Mathematics (MDPI), 2026.
340-/
341theorem RCL_is_unique_functional_form_of_logic
342 (C : ComparisonOperator) (hLaws : SatisfiesLawsOfLogic C) :
343 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
344 HasMultiplicativeConsistency (derivedCost C) P ∧
345 (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
346 obtain ⟨hNorm, _hSym, ⟨P, hPoly, hSymP, hCons⟩, hCont, hNontriv⟩ :=
347 laws_of_logic_imply_dalembert_hypotheses C hLaws
348 obtain ⟨c, hP_form, _⟩ :=
349 bilinear_family_forced (derivedCost C) P hNorm hCons hPoly hSymP hNontriv hCont
350 exact ⟨P, c, hCons, hP_form⟩
351
352/-! ## Cost Corollary: J is the Unique Continuous Cost Function of Logic
353
354The companion uniqueness result for the cost function itself, citing
355`law_of_logic_forces_jcost` from FunctionalEquation.lean. Under the four
356Aristotelian constraints plus the canonical calibration, the unique
357continuous cost on positive ratios is the canonical reciprocal cost
358J(x) = ½(x + 1/x) − 1.
359-/
360
361open Cost Cost.FunctionalEquation in
362/-- **Cost Corollary (J is forced by the laws of logic + calibration)**:
363Under the four Aristotelian constraints, the canonical c = 2 normalization,
364and the unit log-curvature calibration, the unique continuous cost function
365on positive ratios is the canonical reciprocal cost J.
366
367This invokes the peer-reviewed and Lean-verified result:
368
369 Washburn, Zlatanović. "Uniqueness of the Canonical Reciprocal Cost."
370 Mathematics 14 (2026), 935.
371-/
372theorem J_is_unique_cost_under_logic
373 (C : ComparisonOperator) (hLaws : SatisfiesLawsOfLogic C)
374 [AczelSmoothnessPackage]
375 -- The route-independence combiner is the canonical c = 2 RCL.
376 (hRCL : SatisfiesCompositionLaw (derivedCost C))
377 -- The derived cost satisfies the unit log-curvature calibration.
378 (hCalib : IsCalibrated (derivedCost C)) :
379 ∀ x : ℝ, 0 < x → derivedCost C x = Cost.Jcost x := by
380 obtain ⟨hNorm, hSym, _, hCont, _⟩ :=
381 laws_of_logic_imply_dalembert_hypotheses C hLaws
382 -- Express IsSymmetric in the form needed by law_of_logic_forces_jcost.
383 have hRecip : IsReciprocalCost (derivedCost C) := by
384 intro x hx
385 exact hSym x hx
386 exact law_of_logic_forces_jcost (derivedCost C) hRecip hNorm hRCL hCalib hCont
387
388/-! ## Public Law-of-Logic theorem aliases
389
390These theorem-facing names are the canonical public surface for Pith and
391downstream citation pages. The older names above remain in place because they
392describe the proof internals. -/
393
394/-- **Law of Logic forces the Recognition Composition Law**:
395the continuous positive-ratio Law of Logic forces the route-independence
396combiner to have the RCL form `P(u,v) = 2u + 2v + c*u*v`. -/
397theorem law_of_logic_forces_recognition_composition_law
398 (C : ComparisonOperator) (hLogic : LawOfLogic C) :
399 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
400 HasMultiplicativeConsistency (derivedCost C) P ∧
401 (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
402 exact RCL_is_unique_functional_form_of_logic C hLogic
403
404/-- **Law of Logic forces the canonical cost**:
405under the canonical RCL normalization and unit log-curvature calibration, the
406unique continuous positive-ratio cost satisfying the Law of Logic is
407`J(x) = ½(x + x⁻¹) - 1`. -/
408theorem law_of_logic_forces_canonical_cost
409 (C : ComparisonOperator) (hLogic : LawOfLogic C)
410 [Cost.FunctionalEquation.AczelSmoothnessPackage]
411 (hRCL : Cost.FunctionalEquation.SatisfiesCompositionLaw (derivedCost C))
412 (hCalib : Cost.FunctionalEquation.IsCalibrated (derivedCost C)) :
413 ∀ x : ℝ, 0 < x → derivedCost C x = Cost.Jcost x := by
414 exact J_is_unique_cost_under_logic C hLogic hRCL hCalib
415
416/-! ## Summary
417
418The chain established by this module:
419
420 Four Aristotelian laws on a comparison operator
421 ↓ (Translation Theorem, this module)
422 Hypotheses of the d'Alembert Inevitability Theorem
423 ↓ (bilinear_family_forced, Inevitability.lean)
424 Recognition Composition Law: P(u,v) = 2u + 2v + c·uv
425 ↓ (law_of_logic_forces_jcost, FunctionalEquation.lean)
426 Canonical reciprocal cost: J(x) = ½(x + 1/x) − 1
427
428The chain is machine-verified end to end. The Aristotelian framing is
429the only new content of this module; the underlying uniqueness machinery
430is the work of two already-published Mathematics (MDPI) papers.
431
432Polynomiality of the route-independence combiner remains a regularity
433assumption at this level. Level 2 (`Foundation/GeneralizedDAlembert.lean`)
434will close that gap by formalizing the classical continuous-combiner
435classification (Aczél 1966, Kannappan 2009, Stetkær 2013).
436-/
437
438end LogicAsFunctionalEquation
439end Foundation
440end IndisputableMonolith
441