IndisputableMonolith.Algebra.CostAlgebra
IndisputableMonolith/Algebra/CostAlgebra.lean · 988 lines · 94 declarations
show as:
view math explainer →
1/-
2Copyright (c) 2026 Recognition Science. All rights reserved.
3Released under MIT license as described in the file LICENSE.
4Authors: Recognition Science Contributors
5-/
6import Mathlib
7import IndisputableMonolith.Cost
8import IndisputableMonolith.Cost.FunctionalEquation
9import IndisputableMonolith.Cost.FunctionalEquationAczel
10
11/-!
12# Cost Algebra — The Foundational Algebraic Object of Recognition Science
13
14This module formalizes the **cost algebra**: the algebraic structure arising from
15the J-cost function J(x) = ½(x + x⁻¹) − 1 and its Recognition Composition Law.
16
17## The Primitive
18
19The Recognition Composition Law (RCL) is:
20 J(xy) + J(x/y) = 2·J(x)·J(y) + 2·J(x) + 2·J(y)
21
22This is the **one primitive** from which all of Recognition Science flows.
23
24## Algebraic Structure
25
26The cost algebra has several layers:
27
281. **Multiplicative monoid** (ℝ₊, ·, 1) with J as a pseudometric
292. **The RCL as a 2-cocycle condition** — it is a compatibility law
30 for how costs compose under multiplication
313. **Log-coordinate ring** — under t = ln(x), J becomes cosh(t) − 1,
32 and the RCL becomes the standard d'Alembert equation
334. **Reciprocal involution** — x ↦ 1/x is an algebra automorphism
34
35## Key Results (Proved)
36
37- `RCL_holds` : J satisfies the Recognition Composition Law
38- `J_reciprocal_auto` : J(x) = J(1/x) (involution invariance)
39- `J_multiplicative_identity` : J(1) = 0 (identity has zero cost)
40- `costCompose_assoc_defect` : the raw cost-composition associator is `2 * (a - c)`
41- `defectDist_quasi_triangle_local` : local quasi-triangle bound for bounded ratios
42- `ShiftedCarrier` : the shifted operation `A • B = 2AB` is a commutative monoid on `[1/2, ∞)`
43
44## Connection to Full Theory
45
46CostAlgebra is Level 1 of Recognition Algebra:
47 RCL → J unique (T5) → φ forced (T6) → 8-tick (T7) → D=3 (T8) → all physics
48
49Lean module: `IndisputableMonolith.Algebra.CostAlgebra`
50-/
51
52namespace IndisputableMonolith
53namespace Algebra
54namespace CostAlgebra
55
56open Real IndisputableMonolith.Cost
57open IndisputableMonolith.Cost.FunctionalEquation
58
59/-! ## §1. The J-Cost Function as Algebraic Primitive -/
60
61/-- The J-cost function: the unique cost satisfying the Recognition Composition Law.
62 J(x) = ½(x + x⁻¹) − 1 -/
63noncomputable def J (x : ℝ) : ℝ := Jcost x
64
65/-- **Normalization**: The multiplicative identity has zero cost. -/
66theorem J_at_one : J 1 = 0 := Jcost_unit0
67
68/-- **Reciprocal symmetry**: Cost is invariant under inversion.
69 This is the algebraic encoding of "double-entry": every ratio x
70 and its reciprocal 1/x carry the same cost. -/
71theorem J_reciprocal (x : ℝ) (hx : 0 < x) : J x = J x⁻¹ :=
72 Jcost_symm hx
73
74/-- **Non-negativity**: All costs are non-negative on ℝ₊. -/
75theorem J_nonneg (x : ℝ) (hx : 0 < x) : 0 ≤ J x :=
76 Jcost_nonneg hx
77
78/-- **Defect characterization**: J(x) = (x − 1)²/(2x) for x ≠ 0. -/
79theorem J_defect_form (x : ℝ) (hx : x ≠ 0) : J x = (x - 1) ^ 2 / (2 * x) :=
80 Jcost_eq_sq hx
81
82/-! ## §2. The Recognition Composition Law (RCL) -/
83
84/-- The **Recognition Composition Law**: the ONE primitive of Recognition Science.
85
86 J(xy) + J(x/y) = 2·J(x)·J(y) + 2·J(x) + 2·J(y)
87
88 In the log-coordinate form (t = ln x, u = ln y), this becomes:
89 G(t+u) + G(t−u) = 2·G(t)·G(u) + 2·(G(t) + G(u))
90
91 which is a calibrated multiplicative form of the d'Alembert functional equation. -/
92def SatisfiesRCL (F : ℝ → ℝ) : Prop :=
93 ∀ x y : ℝ, 0 < x → 0 < y →
94 F (x * y) + F (x / y) = 2 * F x * F y + 2 * F x + 2 * F y
95
96/-- **THEOREM: J satisfies the RCL.**
97 This is the foundational identity — everything else follows. -/
98theorem RCL_holds : SatisfiesRCL J := by
99 intro x y hx hy
100 unfold J Jcost
101 have hx0 : x ≠ 0 := ne_of_gt hx
102 have hy0 : y ≠ 0 := ne_of_gt hy
103 have hxy0 : x * y ≠ 0 := mul_ne_zero hx0 hy0
104 have hxy_div0 : x / y ≠ 0 := div_ne_zero hx0 hy0
105 field_simp [hx0, hy0, hxy0, hxy_div0]
106 ring
107
108/-! ## §3. Cost Composition as Algebraic Operation -/
109
110/-- **Cost-composition**: The binary operation on costs induced by the RCL.
111 Given two "cost levels" a = J(x) and b = J(y), the composed cost is:
112 a ★ b = 2ab + 2a + 2b = 2(a+1)(b+1) − 2
113
114 This captures how costs combine under multiplication of ratios. -/
115noncomputable def costCompose (a b : ℝ) : ℝ := 2 * a * b + 2 * a + 2 * b
116
117/-- Notation for cost composition -/
118infixl:70 " ★ " => costCompose
119
120/-- **THEOREM: Cost composition is commutative.** -/
121theorem costCompose_comm (a b : ℝ) : a ★ b = b ★ a := by
122 unfold costCompose; ring
123
124/-- **THEOREM: Associator defect for raw RCL composition.**
125 The unnormalized RCL form is not strictly associative; the defect is `2*(a-c)`. -/
126theorem costCompose_assoc_defect (a b c : ℝ) :
127 (a ★ b) ★ c = a ★ (b ★ c) + 2 * (a - c) := by
128 unfold costCompose
129 ring_nf
130
131/-- The raw `★`-operation is flexible. -/
132theorem costCompose_flexible (a b : ℝ) : (a ★ b) ★ a = a ★ (b ★ a) := by
133 simpa using (costCompose_assoc_defect a b a)
134
135/-- **THEOREM: Left-zero evaluation for raw RCL composition.** -/
136theorem costCompose_zero_left (a : ℝ) : (0 : ℝ) ★ a = 2 * a := by
137 unfold costCompose
138 ring_nf
139
140theorem costCompose_zero_right (a : ℝ) : a ★ (0 : ℝ) = 2 * a := by
141 unfold costCompose
142 ring_nf
143
144/-- **THEOREM: Cost composition preserves non-negativity.**
145 If a ≥ 0 and b ≥ 0, then a ★ b ≥ 0. -/
146theorem costCompose_nonneg (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a ★ b := by
147 unfold costCompose
148 have h1 : 0 ≤ 2 * a * b := by positivity
149 have h2 : 0 ≤ 2 * a := by linarith
150 have h3 : 0 ≤ 2 * b := by linarith
151 linarith
152
153/-- **The factored form**: a ★ b = 2(a+1)(b+1) − 2.
154 This reveals the monoid structure: if we set A = a+1, B = b+1,
155 then A ★' B = 2AB − 2, and (A ★' B) + 1 = 2AB − 1. -/
156theorem costCompose_factored (a b : ℝ) :
157 a ★ b = 2 * (a + 1) * (b + 1) - 2 := by
158 unfold costCompose; ring
159
160/-- The nonnegative `★`-magma has no identity element. -/
161theorem costCompose_no_identity :
162 ¬ ∃ e : ℝ, 0 ≤ e ∧ ∀ a : ℝ, 0 ≤ a → e ★ a = a := by
163 intro h
164 rcases h with ⟨e, he_nonneg, he⟩
165 have h0 : e ★ 0 = 0 := he 0 le_rfl
166 rw [costCompose_zero_right] at h0
167 have he0 : e = 0 := by
168 linarith
169 have h1 : (0 : ℝ) ★ 1 = 1 := by
170 simpa [he0] using he 1 (by positivity)
171 rw [costCompose_zero_left] at h1
172 norm_num at h1
173
174/-- Third-power associativity: the triple `★`-power is unambiguous. -/
175theorem costCompose_power_assoc (a : ℝ) : (a ★ a) ★ a = a ★ (a ★ a) := by
176 simpa using (costCompose_flexible a a)
177
178/-- Four copies already witness failure of full power-associativity. -/
179theorem costCompose_fourfold_power_counterexample :
180 (((1 : ℝ) ★ 1) ★ 1) ★ 1 ≠ ((1 : ℝ) ★ 1) ★ ((1 : ℝ) ★ 1) := by
181 norm_num [costCompose]
182
183/-! ## §4. The Shifted Monoid: H = J + 1 -/
184
185/-- The shifted cost: H(x) = J(x) + 1 = ½(x + x⁻¹).
186 Under H, the RCL becomes the standard d'Alembert equation:
187 H(xy) + H(x/y) = 2·H(x)·H(y) -/
188noncomputable def H (x : ℝ) : ℝ := J x + 1
189
190/-- H at identity equals 1. -/
191theorem H_at_one : H 1 = 1 := by
192 unfold H; rw [J_at_one]; ring
193
194/-- **THEOREM: H satisfies the standard d'Alembert equation.**
195 H(xy) + H(x/y) = 2·H(x)·H(y)
196
197 This is the canonical form of the multiplicative d'Alembert
198 functional equation, whose unique continuous solution is cosh. -/
199theorem H_dAlembert (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
200 H (x * y) + H (x / y) = 2 * H x * H y := by
201 unfold H J
202 have rcl := RCL_holds x y hx hy
203 have hsum :
204 Jcost (x * y) + Jcost (x / y) + 2 =
205 2 * Jcost x * Jcost y + 2 * Jcost x + 2 * Jcost y + 2 := by
206 have h' := congrArg (fun z : ℝ => z + 2) rcl
207 simpa [add_assoc, add_left_comm, add_comm] using h'
208 have hmul :
209 2 * (Jcost x + 1) * (Jcost y + 1) =
210 2 * Jcost x * Jcost y + 2 * Jcost x + 2 * Jcost y + 2 := by
211 ring
212 calc
213 Jcost (x * y) + 1 + (Jcost (x / y) + 1)
214 = Jcost (x * y) + Jcost (x / y) + 2 := by ring
215 _ = 2 * Jcost x * Jcost y + 2 * Jcost x + 2 * Jcost y + 2 := hsum
216 _ = 2 * (Jcost x + 1) * (Jcost y + 1) := hmul.symm
217
218/-! ## §4a. The Shifted Monoid on `[1/2, ∞)` -/
219
220/-- The carrier of the shifted monoid from Theorem 2.7:
221 real values bounded below by `1/2`. -/
222abbrev ShiftedCarrier := {A : ℝ // (1 / 2 : ℝ) ≤ A}
223
224/-- The shifted operation `A • B = 2AB` on `[1/2, ∞)`. -/
225def shiftedCompose (A B : ShiftedCarrier) : ShiftedCarrier := by
226 refine ⟨2 * A.1 * B.1, ?_⟩
227 nlinarith [A.2, B.2]
228
229instance : Mul ShiftedCarrier := ⟨shiftedCompose⟩
230
231/-- The identity element `1/2` for the shifted monoid. -/
232noncomputable def shiftedUnit : ShiftedCarrier := ⟨1 / 2, le_rfl⟩
233
234noncomputable instance : One ShiftedCarrier := ⟨shiftedUnit⟩
235
236@[simp] theorem shiftedUnit_val : (shiftedUnit : ℝ) = 1 / 2 := rfl
237
238@[simp] theorem shiftedCompose_val (A B : ShiftedCarrier) :
239 ((A * B : ShiftedCarrier) : ℝ) = 2 * A.1 * B.1 := rfl
240
241noncomputable instance : CommMonoid ShiftedCarrier where
242 mul := (· * ·)
243 mul_assoc A B C := by
244 apply Subtype.ext
245 change 2 * (2 * A.1 * B.1) * C.1 = 2 * A.1 * (2 * B.1 * C.1)
246 ring
247 one := 1
248 one_mul A := by
249 apply Subtype.ext
250 change 2 * (1 / 2 : ℝ) * A.1 = A.1
251 ring
252 mul_one A := by
253 apply Subtype.ext
254 change 2 * A.1 * (1 / 2 : ℝ) = A.1
255 ring
256 mul_comm A B := by
257 apply Subtype.ext
258 change 2 * A.1 * B.1 = 2 * B.1 * A.1
259 ring
260
261/-- `H(x)` lands in `[1, ∞)` on positive reals, hence in `[1/2, ∞)` as well. -/
262theorem H_ge_one (x : ℝ) (hx : 0 < x) : 1 ≤ H x := by
263 unfold H
264 have hJ : 0 ≤ J x := J_nonneg x hx
265 linarith
266
267/-- A positive input determines a canonical shifted-monoid element. -/
268noncomputable def shiftedOfH (x : ℝ) (hx : 0 < x) : ShiftedCarrier :=
269 ⟨H x, by
270 have hHx : 1 ≤ H x := H_ge_one x hx
271 linarith⟩
272
273/-- The narrower `[1, ∞)` range supporting the actual values of `H`. -/
274abbrev ShiftedHValue := {A : ℝ // 1 ≤ A}
275
276/-- The shifted operation is closed on the `H`-value range `[1, ∞)`. -/
277def shiftedComposeH (A B : ShiftedHValue) : ShiftedHValue := by
278 refine ⟨2 * A.1 * B.1, ?_⟩
279 nlinarith [A.2, B.2]
280
281instance : Mul ShiftedHValue := ⟨shiftedComposeH⟩
282
283@[simp] theorem shiftedComposeH_val (A B : ShiftedHValue) :
284 ((A * B : ShiftedHValue) : ℝ) = 2 * A.1 * B.1 := rfl
285
286instance : CommSemigroup ShiftedHValue where
287 mul := (· * ·)
288 mul_assoc A B C := by
289 apply Subtype.ext
290 change 2 * (2 * A.1 * B.1) * C.1 = 2 * A.1 * (2 * B.1 * C.1)
291 ring
292 mul_comm A B := by
293 apply Subtype.ext
294 change 2 * A.1 * B.1 = 2 * B.1 * A.1
295 ring
296
297/-- The `H`-value of a positive real belongs to the closed range `[1, ∞)`. -/
298noncomputable def shiftedHValueOf (x : ℝ) (hx : 0 < x) : ShiftedHValue :=
299 ⟨H x, H_ge_one x hx⟩
300
301/-! ## §5. The Defect Pseudometric -/
302
303/-- **Defect distance**: d(x,y) = J(x/y) measures the "cost of deviation"
304 between two positive reals.
305
306 Properties:
307 - d(x,x) = 0 (identity)
308 - d(x,y) = d(y,x) (symmetry, from J reciprocity)
309 - d(x,y) ≥ 0 (non-negativity) -/
310noncomputable def defectDist (x y : ℝ) : ℝ := J (x / y)
311
312/-- **PROVED: Defect distance is zero at identity.** -/
313theorem defectDist_self (x : ℝ) (hx : 0 < x) : defectDist x x = 0 := by
314 unfold defectDist
315 rw [div_self (ne_of_gt hx)]
316 exact J_at_one
317
318/-- **PROVED: Defect distance is symmetric.** -/
319theorem defectDist_symm (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
320 defectDist x y = defectDist y x := by
321 unfold defectDist
322 have h : x / y > 0 := div_pos hx hy
323 rw [J_reciprocal (x / y) h]
324 congr 1
325 field_simp
326
327/-- **PROVED: Defect distance is non-negative.** -/
328theorem defectDist_nonneg (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
329 0 ≤ defectDist x y :=
330 J_nonneg (x / y) (div_pos hx hy)
331
332/-! ## §5a. Quasi-Triangle Bounds for the Defect Distance -/
333
334/-- On the symmetric interval `[1 / M, M]`, the canonical cost is bounded by
335 its endpoint value `J(M)`. -/
336theorem J_le_J_of_inv_le_le {r M : ℝ} (hM : 1 ≤ M) (hr : 0 < r)
337 (hr_lower : 1 / M ≤ r) (hr_upper : r ≤ M) :
338 J r ≤ J M := by
339 have hMpos : 0 < M := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hM
340 have hfactor :
341 M + M⁻¹ - (r + r⁻¹) = ((M - r) * (M * r - 1)) / (M * r) := by
342 field_simp [hMpos.ne', hr.ne']
343 ring
344 have hMr_ge_one : 1 ≤ M * r := by
345 have hmul := mul_le_mul_of_nonneg_left hr_lower (le_of_lt hMpos)
346 simpa [one_div, hMpos.ne'] using hmul
347 have hnum_nonneg : 0 ≤ (M - r) * (M * r - 1) := by
348 have h1 : 0 ≤ M - r := sub_nonneg.mpr hr_upper
349 have h2 : 0 ≤ M * r - 1 := by linarith
350 exact mul_nonneg h1 h2
351 have hden_pos : 0 < M * r := mul_pos hMpos hr
352 have hsum_le : r + r⁻¹ ≤ M + M⁻¹ := by
353 have hdiff_nonneg : 0 ≤ M + M⁻¹ - (r + r⁻¹) := by
354 rw [hfactor]
355 exact div_nonneg hnum_nonneg (le_of_lt hden_pos)
356 linarith
357 unfold J Jcost
358 linarith
359
360/-- Ratio-bounded pairs have defect at most `J(M)`. -/
361theorem defectDist_le_J_of_ratio_bounds {M x y : ℝ} (hM : 1 ≤ M)
362 (hx : 0 < x) (hy : 0 < y)
363 (hxy_lower : 1 / M ≤ x / y) (hxy_upper : x / y ≤ M) :
364 defectDist x y ≤ J M := by
365 unfold defectDist
366 exact J_le_J_of_inv_le_le hM (div_pos hx hy) hxy_lower hxy_upper
367
368/-- The local quasi-triangle constant from Proposition 2.6. -/
369theorem quasiTriangleConstant_eq (M : ℝ) :
370 2 + J M = (M + 2 + M⁻¹) / 2 := by
371 unfold J Jcost
372 ring
373
374/-- Proposition 2.6, local form: on bounded edge-ratios, the defect distance
375 satisfies the quasi-triangle bound with the paper's constant `K_M`. -/
376theorem defectDist_quasi_triangle_local {M x y z : ℝ} (hM : 1 ≤ M)
377 (hx : 0 < x) (hy : 0 < y) (hz : 0 < z)
378 (hxy_lower : 1 / M ≤ x / y) (hxy_upper : x / y ≤ M)
379 (hyz_lower : 1 / M ≤ y / z) (hyz_upper : y / z ≤ M) :
380 defectDist x z ≤ ((M + 2 + M⁻¹) / 2) * (defectDist x y + defectDist y z) := by
381 have hMpos : 0 < M := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hM
382 have hxy_pos : 0 < x / y := div_pos hx hy
383 have hyz_pos : 0 < y / z := div_pos hy hz
384 have hratio : (x / y) * (y / z) = x / z := by
385 field_simp [hy.ne', hz.ne']
386 have hsub :
387 J ((x / y) * (y / z)) ≤
388 2 * J (x / y) + 2 * J (y / z) + 2 * J (x / y) * J (y / z) := by
389 simpa [J] using (Jcost_submult (x := x / y) (y := y / z) hxy_pos hyz_pos)
390 have hsub' :
391 defectDist x z ≤
392 2 * defectDist x y + 2 * defectDist y z + 2 * defectDist x y * defectDist y z := by
393 unfold defectDist
394 simpa [hratio] using hsub
395 have hxy_bound : defectDist x y ≤ J M :=
396 defectDist_le_J_of_ratio_bounds hM hx hy hxy_lower hxy_upper
397 have hyz_bound : defectDist y z ≤ J M :=
398 defectDist_le_J_of_ratio_bounds hM hy hz hyz_lower hyz_upper
399 have hxy_nonneg : 0 ≤ defectDist x y := defectDist_nonneg x y hx hy
400 have hyz_nonneg : 0 ≤ defectDist y z := defectDist_nonneg y z hy hz
401 have hM_nonneg : 0 ≤ J M := J_nonneg M hMpos
402 have hcross :
403 2 * defectDist x y * defectDist y z ≤ J M * (defectDist x y + defectDist y z) := by
404 have hleft :
405 defectDist x y * defectDist y z ≤ J M * defectDist y z := by
406 exact mul_le_mul_of_nonneg_right hxy_bound hyz_nonneg
407 have hright :
408 defectDist x y * defectDist y z ≤ defectDist x y * J M := by
409 exact mul_le_mul_of_nonneg_left hyz_bound hxy_nonneg
410 have hsum :
411 defectDist x y * defectDist y z + defectDist x y * defectDist y z ≤
412 J M * defectDist y z + defectDist x y * J M := by
413 exact add_le_add hleft hright
414 nlinarith [hsum]
415 calc
416 defectDist x z
417 ≤ 2 * defectDist x y + 2 * defectDist y z + 2 * defectDist x y * defectDist y z := hsub'
418 _ ≤ 2 * defectDist x y + 2 * defectDist y z + J M * (defectDist x y + defectDist y z) := by
419 nlinarith [hcross]
420 _ = (2 + J M) * (defectDist x y + defectDist y z) := by ring
421 _ = ((M + 2 + M⁻¹) / 2) * (defectDist x y + defectDist y z) := by
422 rw [quasiTriangleConstant_eq]
423
424/-- Proposition 2.6, global form: no finite quasi-triangle constant works on
425 all positive triples. -/
426theorem defectDist_no_global_quasi_triangle :
427 ¬ ∃ K : ℝ, 1 < K ∧
428 ∀ x y z : ℝ, 0 < x → 0 < y → 0 < z →
429 defectDist x z ≤ K * (defectDist x y + defectDist y z) := by
430 intro h
431 rcases h with ⟨K, hK, htriangle⟩
432 let r : ℝ := 2 * K
433 have hKpos : 0 < K := lt_trans (by norm_num : (0 : ℝ) < 1) hK
434 have hr : 0 < r := by
435 dsimp [r]
436 positivity
437 have hr_sq : 0 < r ^ 2 := by positivity
438 have hineq := htriangle 1 r (r ^ 2) (by positivity) hr hr_sq
439 have hd1 : defectDist 1 r = J r := by
440 unfold defectDist
441 simpa [one_div] using (J_reciprocal r hr).symm
442 have hd2 : defectDist r (r ^ 2) = J r := by
443 unfold defectDist
444 have hr0 : r ≠ 0 := hr.ne'
445 have hdiv : r / r ^ 2 = r⁻¹ := by
446 rw [pow_two, div_eq_mul_inv]
447 field_simp [hr0]
448 rw [hdiv]
449 exact (J_reciprocal r hr).symm
450 have hd3 : defectDist 1 (r ^ 2) = J (r ^ 2) := by
451 unfold defectDist
452 simpa [one_div] using (J_reciprocal (r ^ 2) hr_sq).symm
453 have hRCL := RCL_holds r r hr hr
454 have hr_div : r / r = 1 := by field_simp [hr.ne']
455 rw [hr_div, J_at_one] at hRCL
456 have hJsq : J (r ^ 2) = 2 * J r * J r + 4 * J r := by
457 have hpow : r * r = r ^ 2 := by ring
458 rw [hpow] at hRCL
459 nlinarith
460 have hineq' : 2 * J r * J r + 4 * J r ≤ K * (2 * J r) := by
461 calc
462 2 * J r * J r + 4 * J r = defectDist 1 (r ^ 2) := by rw [hd3, hJsq]
463 _ ≤ K * (defectDist 1 r + defectDist r (r ^ 2)) := hineq
464 _ = K * (2 * J r) := by rw [hd1, hd2]; ring
465 have hJr_nonneg : 0 ≤ J r := J_nonneg r hr
466 have hJr_ne : J r ≠ 0 := by
467 intro hzero
468 have hr_one : r = 1 := (Jcost_eq_zero_iff r hr).mp (by simpa [J] using hzero)
469 have : (1 : ℝ) < r := by
470 dsimp [r]
471 linarith
472 linarith
473 have hJr_pos : 0 < J r := lt_of_le_of_ne hJr_nonneg (Ne.symm hJr_ne)
474 have hupper : J r + 2 ≤ K := by
475 nlinarith [hineq', hJr_pos]
476 have hJr_eval : J r = K - 1 + 1 / (4 * K) := by
477 dsimp [r]
478 unfold J Jcost
479 field_simp [hKpos.ne']
480 ring
481 have hfrac_pos : 0 < 1 / (4 * K) := by positivity
482 have hlower : K < J r + 2 := by
483 nlinarith [hJr_eval, hfrac_pos]
484 linarith
485
486/-! ## §5b. Left-Cancellation for Raw Cost Composition -/
487
488/-- Subtracting two raw cost-compositions factors through the positive
489 coefficient `2a + 2`. -/
490theorem costCompose_sub_left (a b₁ b₂ : ℝ) :
491 a ★ b₁ - a ★ b₂ = (2 * a + 2) * (b₁ - b₂) := by
492 unfold costCompose
493 ring
494
495/-- Equation (2.6): left-cancellation holds on the nonnegative cost range. -/
496theorem costCompose_left_cancel {a b₁ b₂ : ℝ} (ha : 0 ≤ a)
497 (h : a ★ b₁ = a ★ b₂) : b₁ = b₂ := by
498 have hsub : a ★ b₁ - a ★ b₂ = 0 := sub_eq_zero.mpr h
499 rw [costCompose_sub_left] at hsub
500 have hcoeff : 2 * a + 2 ≠ 0 := by
501 linarith
502 have hdiff : b₁ - b₂ = 0 := by
503 rcases mul_eq_zero.mp hsub with hzero | hzero
504 · exact False.elim (hcoeff hzero)
505 · exact hzero
506 linarith
507
508/-- Right-cancellation follows from commutativity of `★`. -/
509theorem costCompose_right_cancel {a₁ a₂ b : ℝ} (hb : 0 ≤ b)
510 (h : a₁ ★ b = a₂ ★ b) : a₁ = a₂ := by
511 rw [costCompose_comm a₁ b, costCompose_comm a₂ b] at h
512 exact costCompose_left_cancel hb h
513
514/-! ## §5b. Recognition Cost Systems and Window Aggregation -/
515
516/-- The ambient domain of recognition cost systems: positive reals. -/
517def PositiveDomain : Set ℝ := Set.Ioi 0
518
519/-- A recognition cost system packages a ratio cost, a conservation
520 functional, and a finite window length. -/
521structure RecognitionCostSystem (n : ℕ) where
522 cost : ℝ → ℝ
523 rcl : SatisfiesRCL cost
524 sigma : (Fin n → ℝ) → ℝ
525 W : ℕ
526 W_pos : 0 < W
527
528/-- The canonical conservation functional from Definition 2.7:
529 sum of logarithms on positive coordinates. -/
530noncomputable def canonicalSigma {n : ℕ} (x : Fin n → ℝ) : ℝ :=
531 ∑ i, Real.log (x i)
532
533/-- The canonical recognition cost system `(ℝ₊, J, σ, W)`. -/
534noncomputable def canonicalRecognitionCostSystem (n W : ℕ) (hW : 0 < W) :
535 RecognitionCostSystem n where
536 cost := J
537 rcl := RCL_holds
538 sigma := canonicalSigma
539 W := W
540 W_pos := hW
541
542/-- The canonical recognition cost system uses the positive reals as state space. -/
543theorem canonicalRecognitionCostSystem_domain :
544 PositiveDomain = Set.Ioi 0 := rfl
545
546/-- The canonical recognition cost system inherits balance. -/
547theorem canonicalRecognitionCostSystem_cost_one {n W : ℕ} (hW : 0 < W) :
548 (canonicalRecognitionCostSystem n W hW).cost 1 = 0 :=
549 J_at_one
550
551/-- The canonical recognition cost system inherits reciprocal symmetry. -/
552theorem canonicalRecognitionCostSystem_cost_inv {n W : ℕ} (hW : 0 < W)
553 {x : ℝ} (hx : 0 < x) :
554 (canonicalRecognitionCostSystem n W hW).cost x =
555 (canonicalRecognitionCostSystem n W hW).cost x⁻¹ :=
556 J_reciprocal x hx
557
558/-- The one-step shift on sequences. -/
559def seqShift {α : Type*} (y : ℕ → α) : ℕ → α := fun n => y (n + 1)
560
561/-- The `W`-block window-sum operator from Proposition 2.8. -/
562def windowSums {α : Type*} [AddCommMonoid α] (W : ℕ) (y : ℕ → α) : ℕ → α :=
563 fun k => Finset.sum (Finset.range W) (fun j => y (W * k + j))
564
565/-- Shifting the input sequence by one full window shifts the windowed output
566 by one index. -/
567theorem windowSums_shift_equivariant {α : Type*} [AddCommMonoid α]
568 (W : ℕ) (y : ℕ → α) :
569 windowSums W (fun n => y (n + W)) = seqShift (windowSums W y) := by
570 funext k
571 unfold windowSums seqShift
572 refine Finset.sum_congr rfl ?_
573 intro j hj
574 rw [Nat.mul_add, Nat.mul_one]
575 ac_rfl
576
577/-! ## §6. The Cost Algebra Structure -/
578
579/-- **The Cost Algebra**: a structure packaging the complete algebraic data.
580
581 This is the fundamental algebraic object of Recognition Science:
582 - Carrier: ℝ₊ (positive reals)
583 - Binary operation: multiplication (inherited from ℝ)
584 - Cost function: J satisfying RCL
585 - Identity: 1 with J(1) = 0
586 - Involution: x ↦ 1/x preserving J
587
588 From this single structure, all of RS is derived. -/
589structure CostAlgebraData where
590 /-- The cost function -/
591 cost : ℝ → ℝ
592 /-- Satisfies the Recognition Composition Law -/
593 rcl : SatisfiesRCL cost
594 /-- Normalization: cost at identity is zero -/
595 normalized : cost 1 = 0
596 /-- Reciprocal symmetry -/
597 symmetric : ∀ x : ℝ, 0 < x → cost x = cost x⁻¹
598 /-- Non-negativity on ℝ₊ -/
599 nonneg : ∀ x : ℝ, 0 < x → 0 ≤ cost x
600
601/-- **THEOREM: J provides the canonical CostAlgebraData.** -/
602noncomputable def canonicalCostAlgebra : CostAlgebraData where
603 cost := J
604 rcl := RCL_holds
605 normalized := J_at_one
606 symmetric := J_reciprocal
607 nonneg := J_nonneg
608
609/-- **THEOREM: The canonical cost algebra is unique.**
610 Any CostAlgebraData with the same axioms + calibration J''(1)=1
611 must have cost = J. (This is T5 in the forcing chain.) -/
612theorem cost_algebra_unique (C : CostAlgebraData)
613 (hCalib : deriv (deriv (fun t => C.cost (Real.exp t))) 0 = 1)
614 (hCont : ContinuousOn C.cost (Set.Ioi 0))
615 (hSmooth : dAlembert_continuous_implies_smooth_hypothesis (IndisputableMonolith.Cost.FunctionalEquation.H C.cost))
616 (hODE : dAlembert_to_ODE_hypothesis (IndisputableMonolith.Cost.FunctionalEquation.H C.cost))
617 (hContReg : ode_regularity_continuous_hypothesis (IndisputableMonolith.Cost.FunctionalEquation.H C.cost))
618 (hDiffReg : ode_regularity_differentiable_hypothesis (IndisputableMonolith.Cost.FunctionalEquation.H C.cost))
619 (hBoot : ode_linear_regularity_bootstrap_hypothesis (IndisputableMonolith.Cost.FunctionalEquation.H C.cost)) :
620 ∀ x : ℝ, 0 < x → C.cost x = J x := by
621 have hRecip : IsReciprocalCost C.cost := by
622 intro x hx
623 simpa using C.symmetric x hx
624 have hNorm : IsNormalized C.cost := by
625 simpa [IsNormalized] using C.normalized
626 have hComp : SatisfiesCompositionLaw C.cost := by
627 intro x y hx hy
628 exact C.rcl x y hx hy
629 have hCal : IsCalibrated C.cost := by
630 simpa [IsCalibrated, G] using hCalib
631 intro x hx
632 simpa [J] using
633 (washburn_uniqueness C.cost hRecip hNorm hComp hCal hCont
634 hSmooth hODE hContReg hDiffReg hBoot x hx)
635
636/-- **THEOREM (T5, clean form): The canonical cost algebra is unique, via Aczél's theorem.**
637
638 This is the same result as `cost_algebra_unique` but with no regularity hypothesis
639 parameters. The single Aczél axiom (`aczel_dAlembert_smooth`) is used internally
640 by `washburn_uniqueness_aczel`. -/
641theorem cost_algebra_unique_aczel (C : CostAlgebraData)
642 (hCalib : deriv (deriv (fun t => C.cost (Real.exp t))) 0 = 1)
643 (hCont : ContinuousOn C.cost (Set.Ioi 0)) :
644 ∀ x : ℝ, 0 < x → C.cost x = J x := by
645 have hRecip : IsReciprocalCost C.cost := fun x hx => by simpa using C.symmetric x hx
646 have hNorm : IsNormalized C.cost := by simpa [IsNormalized] using C.normalized
647 have hComp : SatisfiesCompositionLaw C.cost := fun x y hx hy => C.rcl x y hx hy
648 have hCal : IsCalibrated C.cost := by simpa [IsCalibrated, G] using hCalib
649 intro x hx
650 simpa [J] using washburn_uniqueness_aczel C.cost hRecip hNorm hComp hCal hCont x hx
651
652/-! ## §7. Morphisms of Cost Algebras -/
653
654/-- A **morphism of cost algebras** is a multiplicative map that preserves cost. -/
655structure CostMorphism (C₁ C₂ : CostAlgebraData) where
656 /-- The underlying map on ℝ₊ -/
657 map : ℝ → ℝ
658 /-- Preserves positivity -/
659 pos : ∀ x, 0 < x → 0 < map x
660 /-- Multiplicative: f(xy) = f(x)·f(y) -/
661 multiplicative : ∀ x y, 0 < x → 0 < y → map (x * y) = map x * map y
662 /-- Preserves cost: C₂.cost(f(x)) = C₁.cost(x) -/
663 preserves_cost : ∀ x, 0 < x → C₂.cost (map x) = C₁.cost x
664
665/-- **THEOREM: The identity is a cost morphism.** -/
666def CostMorphism.id (C : CostAlgebraData) : CostMorphism C C where
667 map := fun x => x
668 pos := fun _ h => h
669 multiplicative := fun _ _ _ _ => rfl
670 preserves_cost := fun _ _ => rfl
671
672/-- **THEOREM: Cost morphisms compose.** -/
673def CostMorphism.comp {C₁ C₂ C₃ : CostAlgebraData}
674 (g : CostMorphism C₂ C₃) (f : CostMorphism C₁ C₂) : CostMorphism C₁ C₃ where
675 map := g.map ∘ f.map
676 pos := fun x hx => g.pos _ (f.pos x hx)
677 multiplicative := fun x y hx hy => by
678 simp [Function.comp]
679 rw [f.multiplicative x y hx hy, g.multiplicative _ _ (f.pos x hx) (f.pos y hy)]
680 preserves_cost := fun x hx => by
681 simp [Function.comp]
682 rw [g.preserves_cost _ (f.pos x hx), f.preserves_cost x hx]
683
684/-! ## §8. The Automorphism Group -/
685
686/-- The **reciprocal automorphism**: x ↦ 1/x.
687 This is the fundamental symmetry of the cost algebra. -/
688noncomputable def reciprocalAuto : ℝ → ℝ := fun x => x⁻¹
689
690/-- **PROVED: The reciprocal map is an involution.** -/
691theorem reciprocal_involution (x : ℝ) :
692 reciprocalAuto (reciprocalAuto x) = x := by
693 unfold reciprocalAuto
694 exact inv_inv x
695
696/-- **PROVED: The reciprocal map preserves J-cost.** -/
697theorem reciprocal_preserves_cost (x : ℝ) (hx : 0 < x) :
698 J (reciprocalAuto x) = J x := by
699 unfold reciprocalAuto
700 exact (J_reciprocal x hx).symm
701
702/-- Exact level-set classification for `J` on positive reals:
703 equal cost means equal ratio or reciprocal ratio. -/
704theorem J_eq_iff_eq_or_inv {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
705 J y = J x ↔ y = x ∨ y = x⁻¹ := by
706 constructor
707 · intro h
708 unfold J Jcost at h
709 have hfrac : y + y⁻¹ = x + x⁻¹ := by linarith
710 have hx0 : x ≠ 0 := ne_of_gt hx
711 have hy0 : y ≠ 0 := ne_of_gt hy
712 field_simp [hx0, hy0] at hfrac
713 have hfactor : (y - x) * (x * y - 1) = 0 := by
714 calc
715 (y - x) * (x * y - 1) = x * y ^ 2 + x - (x ^ 2 * y + y) := by ring
716 _ = 0 := by linarith
717 rcases mul_eq_zero.mp hfactor with hxy | hxy
718 · left
719 linarith
720 · right
721 have hxy1 : x * y = 1 := by linarith
722 calc
723 y = (x⁻¹ * x) * y := by rw [inv_mul_cancel₀ hx0, one_mul]
724 _ = x⁻¹ * (x * y) := by ring
725 _ = x⁻¹ := by rw [hxy1, mul_one]
726 · intro h
727 rcases h with rfl | h
728 · rfl
729 · simpa [h] using (J_reciprocal x hx).symm
730
731/-- The genuine positive domain of the canonical cost algebra. -/
732abbrev PosReal := {x : ℝ // 0 < x}
733
734/-- Multiplication on positive reals. -/
735def posMul (x y : PosReal) : PosReal :=
736 ⟨x.1 * y.1, mul_pos x.2 y.2⟩
737
738/-- Inversion on positive reals. -/
739noncomputable def posInv (x : PosReal) : PosReal :=
740 ⟨x.1⁻¹, inv_pos.mpr x.2⟩
741
742/-- Distinguished positive constants used to close the automorphism proof. -/
743def posOne : PosReal := ⟨1, by norm_num⟩
744def posTwo : PosReal := ⟨2, by norm_num⟩
745noncomputable def posHalf : PosReal := ⟨(1 / 2 : ℝ), by norm_num⟩
746
747@[simp] theorem posInv_inv (x : PosReal) : posInv (posInv x) = x := by
748 apply Subtype.ext
749 simp [posInv]
750
751@[simp] theorem posInv_one : posInv posOne = posOne := by
752 apply Subtype.ext
753 simp [posInv, posOne]
754
755@[simp] theorem posInv_two : posInv posTwo = posHalf := by
756 apply Subtype.ext
757 norm_num [posInv, posTwo, posHalf]
758
759@[simp] theorem posInv_half : posInv posHalf = posTwo := by
760 apply Subtype.ext
761 norm_num [posInv, posTwo, posHalf]
762
763/-- The honest automorphism type of the canonical cost algebra on `ℝ_{>0}`. -/
764def JAut : Type :=
765 { f : PosReal → PosReal //
766 (∀ x y : PosReal, f (posMul x y) = posMul (f x) (f y)) ∧
767 (∀ x : PosReal, J (f x).1 = J x.1) }
768
769namespace JAut
770
771instance : CoeFun JAut (fun _ => PosReal → PosReal) := ⟨fun f => f.1⟩
772
773/-- Multiplicativity of a `J`-automorphism. -/
774theorem multiplicative (f : JAut) (x y : PosReal) :
775 f (posMul x y) = posMul (f x) (f y) :=
776 f.2.1 x y
777
778/-- Cost preservation of a `J`-automorphism. -/
779theorem preserves_cost (f : JAut) (x : PosReal) :
780 J (f x).1 = J x.1 :=
781 f.2.2 x
782
783@[ext] theorem ext {f g : JAut} (h : ∀ x : PosReal, f x = g x) : f = g := by
784 apply Subtype.ext
785 funext x
786 exact h x
787
788/-- The identity automorphism. -/
789def id : JAut :=
790 ⟨fun x => x, by
791 constructor
792 · intro _ _
793 rfl
794 · intro _
795 rfl⟩
796
797/-- The reciprocal automorphism. -/
798noncomputable def reciprocal : JAut :=
799 ⟨posInv, by
800 constructor
801 · intro x y
802 apply Subtype.ext
803 simp [posMul, posInv, mul_comm]
804 · intro x
805 simpa [posInv] using (J_reciprocal x.1 x.2).symm⟩
806
807/-- Composition of `J`-automorphisms. -/
808def comp (g f : JAut) : JAut :=
809 ⟨fun x => g (f x), by
810 constructor
811 · intro x y
812 change g (f (posMul x y)) = posMul (g (f x)) (g (f y))
813 rw [f.multiplicative x y, g.multiplicative (f x) (f y)]
814 · intro x
815 rw [g.preserves_cost (f x), f.preserves_cost x]⟩
816
817@[simp] theorem comp_apply (g f : JAut) (x : PosReal) : comp g f x = g (f x) := rfl
818
819@[simp] theorem comp_id (f : JAut) : comp id f = f := by
820 apply JAut.ext
821 intro x
822 rfl
823
824@[simp] theorem id_comp (f : JAut) : comp f id = f := by
825 apply JAut.ext
826 intro x
827 rfl
828
829@[simp] theorem reciprocal_comp_reciprocal : comp reciprocal reciprocal = id := by
830 apply JAut.ext
831 intro x
832 simp [comp, reciprocal, id]
833
834/-- Pointwise, a `J`-automorphism can only choose the identity branch or the
835 reciprocal branch. -/
836theorem eq_self_or_inv (f : JAut) (x : PosReal) :
837 f x = x ∨ f x = posInv x := by
838 have hJ : J (f x).1 = J x.1 := f.preserves_cost x
839 rcases (J_eq_iff_eq_or_inv x.2 (f x).2).mp hJ with h | h
840 · left
841 exact Subtype.ext h
842 · right
843 exact Subtype.ext h
844
845/-- If `2 * x⁻¹ = 2 * x`, positivity forces `x = 1`. -/
846theorem two_mul_inv_eq_two_mul_iff (x : PosReal) :
847 posMul posTwo (posInv x) = posMul posTwo x ↔ x = posOne := by
848 constructor
849 · intro h
850 apply Subtype.ext
851 have hval : (2 : ℝ) * (x : ℝ)⁻¹ = 2 * (x : ℝ) := congrArg Subtype.val h
852 have hx0 : (x : ℝ) ≠ 0 := ne_of_gt x.2
853 field_simp [hx0] at hval
854 have hsq : (x : ℝ) ^ 2 = 1 := by linarith
855 have hx1 : (x : ℝ) = 1 := by nlinarith [x.2, hsq]
856 simpa [posOne] using hx1
857 · intro h
858 subst x
859 simp [posMul, posInv, posOne, posTwo]
860
861/-- The mixed equation `2 * x⁻¹ = (2x)⁻¹` is impossible on `ℝ_{>0}`. -/
862theorem two_mul_inv_ne_inv_two_mul (x : PosReal) :
863 posMul posTwo (posInv x) ≠ posInv (posMul posTwo x) := by
864 intro h
865 have hval : (2 : ℝ) * (x : ℝ)⁻¹ = ((2 : ℝ) * (x : ℝ))⁻¹ := congrArg Subtype.val h
866 have hx0 : (x : ℝ) ≠ 0 := ne_of_gt x.2
867 field_simp [hx0] at hval
868 norm_num at hval
869
870/-- Any automorphism that fixes `2` is the identity everywhere. -/
871theorem eq_id_of_map_two_eq_two (f : JAut) (h2 : f posTwo = posTwo) : f = id := by
872 apply JAut.ext
873 intro x
874 rcases eq_self_or_inv f x with hfx | hfx
875 · exact hfx
876 · have hmul : f (posMul posTwo x) = posMul posTwo (posInv x) := by
877 calc
878 f (posMul posTwo x) = posMul (f posTwo) (f x) := f.multiplicative posTwo x
879 _ = posMul posTwo (posInv x) := by rw [h2, hfx]
880 rcases eq_self_or_inv f (posMul posTwo x) with htx | htx
881 · have hx1 : x = posOne := (two_mul_inv_eq_two_mul_iff x).mp (hmul.symm.trans htx)
882 subst x
883 simpa [id] using hfx
884 · exact False.elim ((two_mul_inv_ne_inv_two_mul x) (hmul.symm.trans htx))
885
886/-- The reciprocal automorphism is genuinely nontrivial. -/
887theorem reciprocal_ne_id : reciprocal ≠ id := by
888 intro h
889 have htwo : reciprocal posTwo = id posTwo := congrArg (fun f : JAut => f posTwo) h
890 have hval : ((reciprocal posTwo : PosReal) : ℝ) = ((id posTwo : PosReal) : ℝ) :=
891 congrArg Subtype.val htwo
892 norm_num [reciprocal, id, posInv, posTwo] at hval
893
894/-- Exact classification: every `J`-automorphism is either identity or reciprocal. -/
895theorem eq_id_or_reciprocal (f : JAut) : f = id ∨ f = reciprocal := by
896 rcases eq_self_or_inv f posTwo with h2 | h2
897 · left
898 exact eq_id_of_map_two_eq_two f h2
899 · right
900 have hcomp : comp reciprocal f = id := by
901 apply eq_id_of_map_two_eq_two
902 calc
903 comp reciprocal f posTwo = reciprocal (f posTwo) := rfl
904 _ = reciprocal (posInv posTwo) := by rw [h2]
905 _ = posTwo := by simp [reciprocal]
906 apply JAut.ext
907 intro x
908 have hx : comp reciprocal f x = id x := congrArg (fun g : JAut => g x) hcomp
909 have hx' : posInv (posInv (f x)) = posInv x := congrArg posInv hx
910 simpa [comp, reciprocal, id] using hx'
911
912/-- A two-point coding of `Aut(J)`. -/
913noncomputable def equivFinTwo : JAut ≃ Fin 2 := by
914 classical
915 refine
916 { toFun := fun f => if f = id then 0 else 1
917 invFun := fun i => if i = 0 then id else reciprocal
918 left_inv := ?_
919 right_inv := ?_ }
920 · intro f
921 rcases eq_id_or_reciprocal f with h | h
922 · simp [h]
923 · simp [h, reciprocal_ne_id]
924 · intro i
925 fin_cases i <;> simp [reciprocal_ne_id]
926
927/-- **Closed automorphism theorem**: `Aut(J)` is exactly `ℤ/2ℤ`. -/
928noncomputable def equivZModTwo : JAut ≃ ZMod 2 :=
929 equivFinTwo.trans (ZMod.finEquiv 2).toEquiv
930
931end JAut
932
933/-- Paper-facing closed automorphism theorem:
934 the only continuous multiplicative bijections on `ℝ_{>0}` preserving `J`
935 are the identity and reciprocal maps. The continuity and bijectivity
936 assumptions are stronger than needed; the proof uses the sharper `JAut`
937 classification above. -/
938theorem continuous_bijective_preserves_J_eq_id_or_inv
939 {f : PosReal → PosReal} (_hCont : Continuous f) (_hBij : Function.Bijective f)
940 (hmul : ∀ x y : PosReal, f (posMul x y) = posMul (f x) (f y))
941 (hJ : ∀ x : PosReal, J (f x).1 = J x.1) :
942 f = (fun x => x) ∨ f = posInv := by
943 let g : JAut := ⟨f, ⟨hmul, hJ⟩⟩
944 rcases JAut.eq_id_or_reciprocal g with hg | hg
945 · left
946 funext x
947 have hx : g x = JAut.id x := by
948 simpa using congrArg (fun h : JAut => h x) hg
949 simpa [g, JAut.id] using hx
950 · right
951 funext x
952 have hx : g x = JAut.reciprocal x := by
953 simpa using congrArg (fun h : JAut => h x) hg
954 simpa [g, JAut.reciprocal] using hx
955
956/-! ## §9. Summary Certificate -/
957
958/-- **COST ALGEBRA CERTIFICATE**
959
960 The cost algebra packages the foundational algebraic structure:
961 1. J satisfies RCL (the ONE primitive) ✓
962 2. J(1) = 0 (normalization) ✓
963 3. J(x) = J(1/x) (reciprocal symmetry) ✓
964 4. J(x) ≥ 0 on ℝ₊ (non-negativity) ✓
965 5. Raw cost composition is commutative with explicit associator defect ✓
966 6. Left-cancellation holds on the nonnegative cost range ✓
967 7. The shifted operation `A • B = 2AB` is a commutative monoid on `[1/2,∞)` ✓
968 8. H = J+1 satisfies d'Alembert equation ✓
969 9. Uniqueness (T5): J is the UNIQUE solution ✓ (modulo regularity)
970 10. Reciprocal automorphism is an involution ✓ -/
971theorem cost_algebra_certificate :
972 -- RCL holds
973 SatisfiesRCL J ∧
974 -- Normalization
975 J 1 = 0 ∧
976 -- Associator defect is controlled explicitly
977 (∀ a b c : ℝ, (a ★ b) ★ c = a ★ (b ★ c) + 2 * (a - c)) ∧
978 -- Left-cancellation on the nonnegative range
979 (∀ a b₁ b₂ : ℝ, 0 ≤ a → a ★ b₁ = a ★ b₂ → b₁ = b₂) ∧
980 -- H satisfies d'Alembert
981 (∀ x y : ℝ, 0 < x → 0 < y → H (x*y) + H (x/y) = 2 * H x * H y) :=
982 ⟨RCL_holds, J_at_one, costCompose_assoc_defect,
983 fun _ _ _ ha h => costCompose_left_cancel ha h, H_dAlembert⟩
984
985end CostAlgebra
986end Algebra
987end IndisputableMonolith
988