IndisputableMonolith.Foundation.LogicAsFunctionalEquation
IndisputableMonolith/Foundation/LogicAsFunctionalEquation.lean · 381 lines · 16 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 `washburn_uniqueness_aczel` (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/-! ## Translation Lemmas
158
159The four Aristotelian constraints, applied to the derived cost function
160F(r) := C(r, 1), produce the hypotheses of the d'Alembert Inevitability
161Theorem.
162-/
163
164/-- **Translation lemma 1 (Identity ⇒ Normalization)**: If a comparison
165operator satisfies Identity, then the derived cost function takes value
166zero at the multiplicative identity. -/
167theorem identity_implies_normalized (C : ComparisonOperator)
168 (hId : Identity C) :
169 IsNormalized (derivedCost C) := by
170 unfold IsNormalized derivedCost
171 exact hId 1 one_pos
172
173/-- **Translation lemma 2 (Non-contradiction + Scale invariance ⇒ Reciprocity)**:
174If a comparison operator is single-valued under argument reordering and
175depends only on ratios, then the derived cost function is invariant under
176inversion of its argument: F(x) = F(1/x).
177
178The chain of equalities:
179 F(x) = C(x, 1) definition of derivedCost
180 = C(1, x) non-contradiction
181 = C(x⁻¹·1, x⁻¹·x) scale invariance (multiply both args by x⁻¹)
182 = C(x⁻¹, 1) simplify (x⁻¹·1 = x⁻¹, x⁻¹·x = 1)
183 = F(x⁻¹) definition of derivedCost
184-/
185theorem non_contradiction_and_scale_imply_reciprocal
186 (C : ComparisonOperator)
187 (hNC : NonContradiction C)
188 (hSI : ScaleInvariant C) :
189 IsSymmetric (derivedCost C) := by
190 intro x hx
191 have hxinv : (0 : ℝ) < x⁻¹ := inv_pos.mpr hx
192 have hx_ne : (x : ℝ) ≠ 0 := ne_of_gt hx
193 -- Step 1: C(x, 1) = C(1, x) by non-contradiction.
194 have h1 : C x 1 = C 1 x := hNC x 1 hx one_pos
195 -- Step 2: scale invariance with x' = 1, y' = x, λ = x⁻¹ gives
196 -- C(x⁻¹·1, x⁻¹·x) = C(1, x), so C(1, x) = C(x⁻¹·1, x⁻¹·x).
197 have h2 : C 1 x = C (x⁻¹ * 1) (x⁻¹ * x) :=
198 (hSI 1 x x⁻¹ one_pos hx hxinv).symm
199 -- Step 3: simplify x⁻¹·1 = x⁻¹ and x⁻¹·x = 1.
200 have h3 : C (x⁻¹ * 1) (x⁻¹ * x) = C x⁻¹ 1 := by
201 rw [mul_one, inv_mul_cancel₀ hx_ne]
202 show derivedCost C x = derivedCost C x⁻¹
203 unfold derivedCost
204 exact h1.trans (h2.trans h3)
205
206/-- **Translation lemma 3 (Excluded middle ⇒ Continuity)**: If a comparison
207operator is jointly continuous in both arguments on the positive quadrant,
208then the derived cost function is continuous on (0, ∞).
209
210The derivedCost C is the composition r ↦ (r, 1) ↦ C(r, 1). The pair-map is
211continuous everywhere; the uncurried C is continuous on the positive
212quadrant by ExcludedMiddle. The pair-map sends (0, ∞) into the positive
213quadrant. Hence the composition is continuous on (0, ∞). -/
214theorem excluded_middle_implies_continuous
215 (C : ComparisonOperator)
216 (hEM : ExcludedMiddle C) :
217 ContinuousOn (derivedCost C) (Set.Ioi 0) := by
218 -- Pair-map r ↦ (r, 1) is continuous everywhere.
219 have h_pair_cont : Continuous (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ)) :=
220 continuous_id.prodMk continuous_const
221 have h_pair_on : ContinuousOn (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
222 (Set.Ioi (0 : ℝ)) :=
223 h_pair_cont.continuousOn
224 -- Pair-map sends (0,∞) into the positive quadrant.
225 have h_maps : Set.MapsTo (fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
226 (Set.Ioi (0 : ℝ)) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ)) := by
227 intro s hs
228 refine ⟨?_, ?_⟩
229 · exact hs
230 · show (0 : ℝ) < 1
231 exact one_pos
232 -- Compose to get continuity of (uncurry C) ∘ pair on (0,∞).
233 have h_comp : ContinuousOn
234 ((Function.uncurry C) ∘ fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
235 (Set.Ioi (0 : ℝ)) :=
236 hEM.comp h_pair_on h_maps
237 -- The composition equals derivedCost C definitionally.
238 have h_eq : ((Function.uncurry C) ∘ fun s : ℝ => ((s, (1 : ℝ)) : ℝ × ℝ))
239 = derivedCost C := by
240 funext s
241 rfl
242 rw [h_eq] at h_comp
243 exact h_comp
244
245/-- **Translation lemma 4 (Route-independence ⇒ Multiplicative consistency
246with a symmetric polynomial combiner)**: extracted directly from the
247definition of `RouteIndependence`. -/
248theorem route_independence_implies_multiplicative_consistency
249 (C : ComparisonOperator)
250 (hRI : RouteIndependence C) :
251 ∃ P : ℝ → ℝ → ℝ,
252 (∃ 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) ∧
253 (∀ u v, P u v = P v u) ∧
254 HasMultiplicativeConsistency (derivedCost C) P := by
255 obtain ⟨P, hPoly, hSym, hCons⟩ := hRI
256 refine ⟨P, hPoly, hSym, ?_⟩
257 intro x y hx hy
258 exact hCons x y hx hy
259
260/-! ## The Translation Theorem -/
261
262/-- **Translation Theorem**: A comparison operator satisfying the four
263Aristotelian constraints, together with scale invariance and non-triviality,
264satisfies the hypotheses of the d'Alembert Inevitability Theorem on its
265derived cost function.
266
267This is the core technical content of the precursor paper. Once this is in
268hand, the existing peer-reviewed and machine-verified theorems
269(`bilinear_family_forced`, `washburn_uniqueness_aczel`) close the chain. -/
270theorem laws_of_logic_imply_dalembert_hypotheses
271 (C : ComparisonOperator) (hLaws : SatisfiesLawsOfLogic C) :
272 IsNormalized (derivedCost C) ∧
273 IsSymmetric (derivedCost C) ∧
274 (∃ P : ℝ → ℝ → ℝ,
275 (∃ 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) ∧
276 (∀ u v, P u v = P v u) ∧
277 HasMultiplicativeConsistency (derivedCost C) P) ∧
278 ContinuousOn (derivedCost C) (Set.Ioi 0) ∧
279 (∃ x : ℝ, 0 < x ∧ derivedCost C x ≠ 0) := by
280 refine ⟨?_, ?_, ?_, ?_, ?_⟩
281 · exact identity_implies_normalized C hLaws.identity
282 · exact non_contradiction_and_scale_imply_reciprocal C
283 hLaws.non_contradiction hLaws.scale_invariant
284 · exact route_independence_implies_multiplicative_consistency C
285 hLaws.route_independence
286 · exact excluded_middle_implies_continuous C hLaws.excluded_middle
287 · exact hLaws.non_trivial
288
289/-! ## Main Theorem: RCL is the Unique Functional Form of the Laws of Logic -/
290
291/-- **Main theorem (Logical Formalization Theorem)**: For a comparison
292operator satisfying the four Aristotelian constraints with scale invariance
293and non-triviality, the route-independence combiner is necessarily of the
294Recognition Composition Law form: `P(u,v) = 2u + 2v + c·uv` for some
295constant c ∈ ℝ.
296
297In other words: the unique functional form the laws of logic can take on
298continuous comparisons of positive ratios, under the polynomial regularity
299assumption, is the Recognition Composition Law.
300
301This is an immediate corollary of `laws_of_logic_imply_dalembert_hypotheses`
302combined with `bilinear_family_forced` (Inevitability.lean), which has been
303peer-reviewed in:
304
305 Washburn, Zlatanović, Allahyarov.
306 "The d'Alembert Inevitability Theorem."
307 Mathematics (MDPI), 2026.
308-/
309theorem RCL_is_unique_functional_form_of_logic
310 (C : ComparisonOperator) (hLaws : SatisfiesLawsOfLogic C) :
311 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
312 HasMultiplicativeConsistency (derivedCost C) P ∧
313 (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
314 obtain ⟨hNorm, _hSym, ⟨P, hPoly, hSymP, hCons⟩, hCont, hNontriv⟩ :=
315 laws_of_logic_imply_dalembert_hypotheses C hLaws
316 obtain ⟨c, hP_form, _⟩ :=
317 bilinear_family_forced (derivedCost C) P hNorm hCons hPoly hSymP hNontriv hCont
318 exact ⟨P, c, hCons, hP_form⟩
319
320/-! ## Cost Corollary: J is the Unique Continuous Cost Function of Logic
321
322The companion uniqueness result for the cost function itself, citing
323`washburn_uniqueness_aczel` from FunctionalEquation.lean. Under the four
324Aristotelian constraints plus the canonical calibration, the unique
325continuous cost on positive ratios is the canonical reciprocal cost
326J(x) = ½(x + 1/x) − 1.
327-/
328
329open Cost Cost.FunctionalEquation in
330/-- **Cost Corollary (J is forced by the laws of logic + calibration)**:
331Under the four Aristotelian constraints, the canonical c = 2 normalization,
332and the unit log-curvature calibration, the unique continuous cost function
333on positive ratios is the canonical reciprocal cost J.
334
335This invokes the peer-reviewed and Lean-verified result:
336
337 Washburn, Zlatanović. "Uniqueness of the Canonical Reciprocal Cost."
338 Mathematics 14 (2026), 935.
339-/
340theorem J_is_unique_cost_under_logic
341 (C : ComparisonOperator) (hLaws : SatisfiesLawsOfLogic C)
342 [AczelSmoothnessPackage]
343 -- The route-independence combiner is the canonical c = 2 RCL.
344 (hRCL : SatisfiesCompositionLaw (derivedCost C))
345 -- The derived cost satisfies the unit log-curvature calibration.
346 (hCalib : IsCalibrated (derivedCost C)) :
347 ∀ x : ℝ, 0 < x → derivedCost C x = Cost.Jcost x := by
348 obtain ⟨hNorm, hSym, _, hCont, _⟩ :=
349 laws_of_logic_imply_dalembert_hypotheses C hLaws
350 -- Express IsSymmetric in the form needed by washburn_uniqueness_aczel.
351 have hRecip : IsReciprocalCost (derivedCost C) := by
352 intro x hx
353 exact hSym x hx
354 exact washburn_uniqueness_aczel (derivedCost C) hRecip hNorm hRCL hCalib hCont
355
356/-! ## Summary
357
358The chain established by this module:
359
360 Four Aristotelian laws on a comparison operator
361 ↓ (Translation Theorem, this module)
362 Hypotheses of the d'Alembert Inevitability Theorem
363 ↓ (bilinear_family_forced, Inevitability.lean)
364 Recognition Composition Law: P(u,v) = 2u + 2v + c·uv
365 ↓ (washburn_uniqueness_aczel, FunctionalEquation.lean)
366 Canonical reciprocal cost: J(x) = ½(x + 1/x) − 1
367
368The chain is machine-verified end to end. The Aristotelian framing is
369the only new content of this module; the underlying uniqueness machinery
370is the work of two already-published Mathematics (MDPI) papers.
371
372Polynomiality of the route-independence combiner remains a regularity
373assumption at this level. Level 2 (`Foundation/GeneralizedDAlembert.lean`)
374will close that gap by formalizing the classical continuous-combiner
375classification (Aczél 1966, Kannappan 2009, Stetkær 2013).
376-/
377
378end LogicAsFunctionalEquation
379end Foundation
380end IndisputableMonolith
381