IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCMonotoneDAlembert

   1/-
   2  PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
   3
   4  The completeness-free d'Alembert machinery, and the cost-forcing theorem it
   5  buys, living where the forcing chain can reach them.
   6
   7  These declarations were part of `PRCNativeCostUniqueness`, which also carries
   8  the whole completion apparatus (Cauchy reals, trace closure, the ratio-orbit
   9  carrier). That made them unreachable from `Foundation.UnifiedForcingChain`:
  10  citing them would have inverted the dependency order and dragged the
  11  completion machinery underneath the chain that is supposed to be beneath it.
  12  So the chain went on stating its cost rung T5 with an `AczelSmoothnessPackage`
  13  instance plus `ContinuousOn`, two continuum inputs, while the proof that
  14  neither is needed sat one module away and uncited.
  15
  16  Nothing here mentions the carrier, the completion, or `costLambda`. Every
  17  declaration is a statement about a real function satisfying the d'Alembert
  18  identity, so the only imports are Mathlib and the cost functional equation.
  19  `PRCNativeCostUniqueness` now imports this file, and since the namespace is
  20  unchanged (`PRCJCost`), no call site anywhere moved.
  21
  22  The block below is verbatim from its previous home. What is new is at the
  23  bottom: `cosh_scale_curvature`, the log-coordinate facts about `Cost.Jcost`,
  24  and `jcost_forced_by_order`, which routes straight from the cosh family to `J`
  25  without passing through `costLambda`. That last detour is why the theorem
  26  could not previously be stated below the completion layer.
  27-/
  28
  29import Mathlib
  30import IndisputableMonolith.Cost
  31import IndisputableMonolith.Cost.FunctionalEquation
  32
  33namespace IndisputableMonolith
  34namespace Foundation
  35namespace PrimitiveRecognitionCalculus
  36namespace PRCJCost
  37
  38/-! ## The completeness-free d'Alembert block -/
  39
  40/-- **§9 regularity-substitute brick (completeness-free): a monotone additive
  41real function is linear.**
  42
  43The classical J-uniqueness theorem (`law_of_logic_forces_jcost`) uses
  44`ContinuousOn`, an analytic hypothesis that presupposes the continuum. The §9
  45question asked whether that analytic input can be replaced by a purely
  46order-theoretic one available on any Archimedean ordered field *without*
  47completeness. That question is now CLOSED in the positive direction: the
  48completeness-free cost forcing is assembled below as `dAlembert_cosh_of_monotone`
  49(even, normalized, monotone d'Alembert solution is `cosh ∘ linear`) and
  50`composition_law_monotone_forces_costLambda` (the real cost hypotheses plus
  51`MonotoneOn` force the scale family), with faithfulness `costLambda_injOn_pos`.
  52
  53This theorem is the load-bearing regularity brick those results consume: a
  54`Monotone` solution of Cauchy's additive equation `f (x+y) = f x + f y` is forced
  55to be linear, `f x = f 1 · x`. The proof uses only the density of `ℚ` in an
  56Archimedean field (`exists_rat_btwn`), never the least-upper-bound axiom. So
  57monotonicity is a genuine completeness-free substitute for continuity at the
  58additive layer that the d'Alembert reduction of the RCL lands on (set `g = F+1`,
  59`h(t) = g(e^t)`, then `h(s+t)+h(s−t) = 2 h(s) h(t)` with even `h` of the form
  60`cosh ∘ (additive)`; a monotone such `h` forces the inner additive map linear).
  61With the assembly complete, the continuum posit dissolves for the cost form:
  62the framework's arbitrary content on the cost side drops to one unit of scale. -/
  63theorem monotone_additive_isLinear {f : ℝ → ℝ}
  64    (hadd : ∀ x y, f (x + y) = f x + f y) (hmono : Monotone f) :
  65    ∀ x, f x = f 1 * x := by
  66  have hf0 : f 0 = 0 := by
  67    have h := hadd 0 0
  68    rw [add_zero] at h
  69    linarith
  70  let F : ℝ →+ ℝ := AddMonoidHom.mk' f (fun a b => hadd a b)
  71  have hFcoe : ∀ y, F y = f y := fun _ => rfl
  72  have hFq : ∀ q : ℚ, f (q : ℝ) = f 1 * (q : ℝ) := by
  73    intro q
  74    have h := map_ratCast_smul F ℝ ℝ q (1 : ℝ)
  75    simp only [smul_eq_mul, mul_one, hFcoe] at h
  76    rw [h]; ring
  77  intro x
  78  set c := f 1 with hc_def
  79  have hc : 0 ≤ c := by
  80    have hmle : f 0 ≤ f 1 := hmono (by norm_num)
  81    rw [hf0] at hmle; exact hmle
  82  rcases eq_or_lt_of_le hc with hc0 | hcpos
  83  · -- c = 0: f is identically 0, and 0 = c * x
  84    have hub : f x ≤ 0 := by
  85      obtain ⟨r, hxr, -⟩ := exists_rat_btwn (lt_add_one x)
  86      have hmr := hmono hxr.le
  87      rw [hFq r, ← hc0, zero_mul] at hmr
  88      exact hmr
  89    have hlb : 0 ≤ f x := by
  90      obtain ⟨q, -, hqx⟩ := exists_rat_btwn (sub_one_lt x)
  91      have hmq := hmono hqx.le
  92      rw [hFq q, ← hc0, zero_mul] at hmq
  93      exact hmq
  94    rw [← hc0, zero_mul]
  95    linarith
  96  · -- c > 0: Archimedean squeeze pins f x = c * x
  97    refine le_antisymm ?_ ?_
  98    · by_contra hcon
  99      push_neg at hcon
 100      have hxlt : x < f x / c := by
 101        rw [lt_div_iff₀ hcpos]; linarith [mul_comm c x]
 102      obtain ⟨r, hxr, hrlt⟩ := exists_rat_btwn hxlt
 103      have h1 : f x ≤ c * (r : ℝ) := by
 104        have hm := hmono hxr.le; rwa [hFq r] at hm
 105      have h2 : c * (r : ℝ) < f x := by
 106        have := (lt_div_iff₀ hcpos).mp hrlt; linarith [mul_comm (r : ℝ) c]
 107      linarith
 108    · by_contra hcon
 109      push_neg at hcon
 110      have hxlt : f x / c < x := by
 111        rw [div_lt_iff₀ hcpos]; linarith [mul_comm c x]
 112      obtain ⟨q, hqlt, hqx⟩ := exists_rat_btwn hxlt
 113      have h1 : c * (q : ℝ) ≤ f x := by
 114        have hm := hmono hqx.le; rwa [hFq q] at hm
 115      have h2 : f x < c * (q : ℝ) := by
 116        have := (div_lt_iff₀ hcpos).mp hqlt; linarith [mul_comm (q : ℝ) c]
 117      linarith
 118
 119/-- **Nonnegative version: additive-on-`[0,∞)` + monotone ⇒ linear on `[0,∞)`.**
 120A function additive for nonnegative arguments and monotone on `[0,∞)` with
 121`f 0 = 0` satisfies `f t = f 1 · t` for `t ≥ 0`. Proved by the odd extension to
 122all of `ℝ` plus `monotone_additive_isLinear`; completeness-free. This is the form
 123the `log∘φ` exponent of the d'Alembert/monotone route actually has (additivity
 124only comes from `φ(s+t)=φ(s)φ(t)` for nonnegative `s,t`). -/
 125theorem monotone_additive_nonneg_isLinear {f : ℝ → ℝ}
 126    (hadd : ∀ a b, 0 ≤ a → 0 ≤ b → f (a + b) = f a + f b)
 127    (hmono : MonotoneOn f (Set.Ici (0 : ℝ))) (hf0 : f 0 = 0) :
 128    ∀ t, 0 ≤ t → f t = f 1 * t := by
 129  classical
 130  have hsub : ∀ a b, 0 ≤ b → b ≤ a → f (a - b) = f a - f b := by
 131    intro a b hb hba
 132    have h := hadd (a - b) b (by linarith) hb
 133    rw [sub_add_cancel] at h
 134    linarith
 135  set g : ℝ → ℝ := fun t => if 0 ≤ t then f t else - f (-t) with hg
 136  have hg_pos : ∀ t, 0 ≤ t → g t = f t := by intro t ht; simp [hg, ht]
 137  have hg_neg : ∀ t, t < 0 → g t = - f (-t) := by
 138    intro t ht; simp [hg, not_le.mpr ht]
 139  have hgadd : ∀ s t, g (s + t) = g s + g t := by
 140    intro s t
 141    rcases le_or_lt 0 s with hs | hs <;> rcases le_or_lt 0 t with ht | ht
 142    · rw [hg_pos s hs, hg_pos t ht, hg_pos (s + t) (by linarith), hadd s t hs ht]
 143    · rw [hg_pos s hs, hg_neg t ht]
 144      rcases le_or_lt 0 (s + t) with hst | hst
 145      · rw [hg_pos (s + t) hst]
 146        have hh := hsub s (-t) (by linarith) (by linarith)
 147        rw [sub_neg_eq_add] at hh
 148        rw [hh]; ring
 149      · rw [hg_neg (s + t) hst]
 150        have hh := hsub (-t) s (by linarith) (by linarith)
 151        rw [show -t - s = -(s + t) by ring] at hh
 152        rw [hh]; ring
 153    · rw [hg_neg s hs, hg_pos t ht]
 154      rcases le_or_lt 0 (s + t) with hst | hst
 155      · rw [hg_pos (s + t) hst]
 156        have hh := hsub t (-s) (by linarith) (by linarith)
 157        rw [show t - -s = s + t by ring] at hh
 158        rw [hh]; ring
 159      · rw [hg_neg (s + t) hst]
 160        have hh := hsub (-s) t (by linarith) (by linarith)
 161        rw [show -s - t = -(s + t) by ring] at hh
 162        rw [hh]; ring
 163    · rw [hg_neg s hs, hg_neg t ht, hg_neg (s + t) (by linarith),
 164        show -(s + t) = (-s) + (-t) by ring, hadd (-s) (-t) (by linarith) (by linarith)]
 165      ring
 166  have hgmono : Monotone g := by
 167    intro x y hxy
 168    rcases le_or_lt 0 x with hx | hx
 169    · have hy : 0 ≤ y := le_trans hx hxy
 170      rw [hg_pos x hx, hg_pos y hy]
 171      exact hmono (Set.mem_Ici.mpr hx) (Set.mem_Ici.mpr hy) hxy
 172    · rcases le_or_lt 0 y with hy | hy
 173      · rw [hg_neg x hx, hg_pos y hy]
 174        have hfnx : f 0 ≤ f (-x) :=
 175          hmono (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr (by linarith)) (by linarith)
 176        have hfy : f 0 ≤ f y :=
 177          hmono (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr hy) hy
 178        rw [hf0] at hfnx hfy
 179        linarith
 180      · rw [hg_neg x hx, hg_neg y hy]
 181        have hle : f (-y) ≤ f (-x) :=
 182          hmono (Set.mem_Ici.mpr (by linarith)) (Set.mem_Ici.mpr (by linarith)) (by linarith)
 183        linarith
 184  have hlin := monotone_additive_isLinear hgadd hgmono
 185  have hg1 : g 1 = f 1 := hg_pos 1 (by norm_num)
 186  intro t ht
 187  have hlt := hlin t
 188  rw [hg_pos t ht, hg1] at hlt
 189  exact hlt
 190
 191/-- **§9 order-only constraint 1 (completeness-free): d'Alembert duplication.**
 192A solution of the d'Alembert equation `H(s+t)+H(s−t)=2 H s · H t` with `H 0 = 1`
 193satisfies `H(2t) = 2 (H t)^2 − 1` — the cosh duplication formula, derived as pure
 194algebra from the equation. No regularity, no completeness. -/
 195theorem dAlembert_duplication {H : ℝ → ℝ}
 196    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1) :
 197    ∀ t, H (2 * t) = 2 * (H t) ^ 2 - 1 := by
 198  intro t
 199  have h := hd t t
 200  rw [sub_self, h0] at h
 201  rw [two_mul, pow_two]
 202  linarith
 203
 204/-- **§9 order-only constraint 2 (completeness-free): the cosh floor `H ≥ 1`.**
 205A d'Alembert solution that is monotone on `[0,∞)` with `H 0 = 1` stays `≥ 1`
 206there. The floor is forced by order alone: monotonicity from the base value `1`
 207gives it in one step. This excludes the bounded "cosine" branch `H = cos(c·)` of
 208d'Alembert (which dips below `1`) using no analytic input, isolating the
 209unbounded cosh branch as the only order-compatible family — the first place the
 210§9 monotone route does real work that continuity used to do. -/
 211theorem dAlembert_ge_one_of_monotone {H : ℝ → ℝ}
 212    (h0 : H 0 = 1) (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
 213    ∀ t, 0 ≤ t → 1 ≤ H t := by
 214  intro t ht
 215  have hle := hmono Set.left_mem_Ici (Set.mem_Ici.mpr ht) ht
 216  rwa [h0] at hle
 217
 218/-- **Product identity from d'Alembert.** Applying the equation to arguments
 219`(s+t)` and `(s−t)` (whose sum is `2s` and difference is `2t`) gives
 220`H(2s)+H(2t) = 2 H(s+t) H(s−t)`. Pure algebra, no regularity. -/
 221theorem dAlembert_prod {H : ℝ → ℝ}
 222    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) :
 223    ∀ s t, H (2 * s) + H (2 * t) = 2 * H (s + t) * H (s - t) := by
 224  intro s t
 225  have h := hd (s + t) (s - t)
 226  have e1 : (s + t) + (s - t) = 2 * s := by ring
 227  have e2 : (s + t) - (s - t) = 2 * t := by ring
 228  rw [e1, e2] at h
 229  linarith
 230
 231/-- **§9 sign crux, magnitude half: difference square.** Combining the sum law,
 232the product identity and the duplication formula forces
 233`(H(s+t) − H(s−t))² = 4 (H(s)²−1)(H(t)²−1)`. Pure algebra, completeness-free.
 234This is the "sinh²" relation; only the SIGN of the square root is left, and that
 235is what monotonicity fixes in `dAlembert_diff_eq_of_monotone`. -/
 236theorem dAlembert_diff_sq {H : ℝ → ℝ}
 237    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1) :
 238    ∀ s t, (H (s + t) - H (s - t)) ^ 2
 239        = 4 * ((H s) ^ 2 - 1) * ((H t) ^ 2 - 1) := by
 240  intro s t
 241  have hsum := hd s t
 242  have hprod := dAlembert_prod hd s t
 243  have hds := dAlembert_duplication hd h0 s
 244  have hdt := dAlembert_duplication hd h0 t
 245  rw [hds, hdt] at hprod
 246  have expand : (H (s + t) - H (s - t)) ^ 2
 247      = (H (s + t) + H (s - t)) ^ 2 - 2 * (2 * H (s + t) * H (s - t)) := by ring
 248  rw [expand, hsum, ← hprod]
 249  ring
 250
 251/-- **§9 sign crux, RESOLVED: monotonicity fixes the sign.** For `0 ≤ t ≤ s`,
 252both `s+t` and `s−t` lie in `[0,∞)`, so monotonicity of `H` there forces
 253`H(s+t) ≥ H(s−t)`; the difference is the NONNEGATIVE root of the square computed
 254in `dAlembert_diff_sq`:
 255
 256`H(s+t) − H(s−t) = 2 √(H(s)²−1) · √(H(t)²−1)`.
 257
 258This is the cosh addition formula `cosh(a+b) − cosh(a−b) = 2 sinh a sinh b` with
 259`sinh = √(cosh²−1) ≥ 0`. The sign — the one place the analytic proof used
 260continuity — is here pinned by ORDER ALONE. So the answer to the §9 sub-question
 261"can monotonicity fix the sign?" is YES. Completeness is not needed for this
 262step; only the order structure of the field is. -/
 263theorem dAlembert_diff_eq_of_monotone {H : ℝ → ℝ}
 264    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
 265    (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
 266    ∀ s t, 0 ≤ t → t ≤ s →
 267      H (s + t) - H (s - t)
 268        = 2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1) := by
 269  intro s t ht hts
 270  have hs0 : 0 ≤ s := le_trans ht hts
 271  have hge1s : 1 ≤ H s := dAlembert_ge_one_of_monotone h0 hmono s hs0
 272  have hge1t : 1 ≤ H t := dAlembert_ge_one_of_monotone h0 hmono t ht
 273  have hSs : 0 ≤ (H s) ^ 2 - 1 := by nlinarith [hge1s]
 274  have hSt : 0 ≤ (H t) ^ 2 - 1 := by nlinarith [hge1t]
 275  have hsmt_nonneg : 0 ≤ s - t := by linarith
 276  have hspt_nonneg : 0 ≤ s + t := by linarith
 277  have hdiff_nonneg : 0 ≤ H (s + t) - H (s - t) := by
 278    have hle : H (s - t) ≤ H (s + t) :=
 279      hmono (Set.mem_Ici.mpr hsmt_nonneg) (Set.mem_Ici.mpr hspt_nonneg) (by linarith)
 280    linarith
 281  have hrhs_nonneg :
 282      0 ≤ 2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1) := by positivity
 283  have hsq := dAlembert_diff_sq hd h0 s t
 284  have hrhs_sq :
 285      (2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1)) ^ 2
 286        = 4 * ((H s) ^ 2 - 1) * ((H t) ^ 2 - 1) := by
 287    rw [show (2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1)) ^ 2
 288          = 4 * (Real.sqrt ((H s) ^ 2 - 1)) ^ 2 * (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 by ring,
 289       Real.sq_sqrt hSs, Real.sq_sqrt hSt]
 290  have hsquares :
 291      (H (s + t) - H (s - t)) ^ 2
 292        = (2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1)) ^ 2 := by
 293    rw [hsq, hrhs_sq]
 294  have hsqrt := congrArg Real.sqrt hsquares
 295  rwa [Real.sqrt_sq hdiff_nonneg, Real.sqrt_sq hrhs_nonneg] at hsqrt
 296
 297/-- **Cosh addition formula, monotone-fixed sign.** For `0 ≤ t ≤ s`,
 298`H(s+t) = H s · H t + √(H s²−1)·√(H t²−1)`, the half-sum of the sum law and the
 299sign-fixed difference law. Completeness-free. This is the multiplicative seed:
 300with `φ(x) = H x + √(H x²−1)`, this and the matching `S`-addition identity give
 301`φ(s+t) = φ(s)·φ(t)`, i.e. `log ∘ φ` is additive — and monotone, hence linear by
 302`monotone_additive_isLinear`, hence `H = cosh(linear)` with no completeness. -/
 303theorem dAlembert_add_of_monotone {H : ℝ → ℝ}
 304    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
 305    (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
 306    ∀ s t, 0 ≤ t → t ≤ s →
 307      H (s + t)
 308        = H s * H t + Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1) := by
 309  intro s t ht hts
 310  have hsum := hd s t
 311  have hdiff := dAlembert_diff_eq_of_monotone hd h0 hmono s t ht hts
 312  have e : 2 * H (s + t) = (H (s + t) + H (s - t)) + (H (s + t) - H (s - t)) := by ring
 313  rw [hsum, hdiff] at e
 314  linear_combination e / 2
 315
 316/-- **`S`-addition identity (monotone-fixed).** With `S x = √(H x²−1)`, for
 317`0 ≤ t ≤ s` the "sinh" addition formula `S(s+t) = H s · S t + S s · H t` holds.
 318Proved by squaring (using the `H`-addition formula) and taking nonnegative roots.
 319Completeness-free. -/
 320theorem dAlembert_S_add_of_monotone {H : ℝ → ℝ}
 321    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
 322    (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
 323    ∀ s t, 0 ≤ t → t ≤ s →
 324      Real.sqrt ((H (s + t)) ^ 2 - 1)
 325        = H s * Real.sqrt ((H t) ^ 2 - 1) + Real.sqrt ((H s) ^ 2 - 1) * H t := by
 326  intro s t ht hts
 327  have hge1s : 1 ≤ H s := dAlembert_ge_one_of_monotone h0 hmono s (le_trans ht hts)
 328  have hge1t : 1 ≤ H t := dAlembert_ge_one_of_monotone h0 hmono t ht
 329  have hHs0 : 0 ≤ H s := by linarith
 330  have hHt0 : 0 ≤ H t := by linarith
 331  have hSs : 0 ≤ (H s) ^ 2 - 1 := by nlinarith [hge1s]
 332  have hSt : 0 ≤ (H t) ^ 2 - 1 := by nlinarith [hge1t]
 333  have hadd := dAlembert_add_of_monotone hd h0 hmono s t ht hts
 334  have hu := Real.sq_sqrt hSs
 335  have hv := Real.sq_sqrt hSt
 336  have hrhs_nonneg :
 337      0 ≤ H s * Real.sqrt ((H t) ^ 2 - 1) + Real.sqrt ((H s) ^ 2 - 1) * H t := by
 338    have t1 : 0 ≤ H s * Real.sqrt ((H t) ^ 2 - 1) := mul_nonneg hHs0 (Real.sqrt_nonneg _)
 339    have t2 : 0 ≤ Real.sqrt ((H s) ^ 2 - 1) * H t := mul_nonneg (Real.sqrt_nonneg _) hHt0
 340    linarith
 341  have rhs_sq :
 342      (H s * Real.sqrt ((H t) ^ 2 - 1) + Real.sqrt ((H s) ^ 2 - 1) * H t) ^ 2
 343        = (H (s + t)) ^ 2 - 1 := by
 344    rw [hadd]
 345    linear_combination ((H t) ^ 2 - (Real.sqrt ((H t) ^ 2 - 1)) ^ 2) * hu + hv
 346  rw [← rhs_sq]
 347  exact Real.sqrt_sq hrhs_nonneg
 348
 349/-- **`φ` is multiplicative (monotone route).** With `φ x = H x + √(H x²−1)`, for
 350`0 ≤ t ≤ s` we have `φ(s+t) = φ(s)·φ(t)`. This is the `H`-addition and
 351`S`-addition identities packaged as a single product law. `φ > 0`, so `log ∘ φ`
 352is additive on `[0,∞)`; it is also monotone (both `H` and `S` increase there),
 353hence linear by `monotone_additive_isLinear`. That linear exponent makes
 354`H = cosh(c·)`, completing the completeness-free cost-form derivation. -/
 355theorem phi_mul_of_monotone {H : ℝ → ℝ}
 356    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
 357    (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
 358    ∀ s t, 0 ≤ t → t ≤ s →
 359      H (s + t) + Real.sqrt ((H (s + t)) ^ 2 - 1)
 360        = (H s + Real.sqrt ((H s) ^ 2 - 1)) * (H t + Real.sqrt ((H t) ^ 2 - 1)) := by
 361  intro s t ht hts
 362  have h1 := dAlembert_add_of_monotone hd h0 hmono s t ht hts
 363  have h2 := dAlembert_S_add_of_monotone hd h0 hmono s t ht hts
 364  rw [h2, h1]; ring
 365
 366/-- **§9 RESOLVED, POSITIVE: the cosh cost form is forced WITHOUT completeness.**
 367
 368A solution `H` of the d'Alembert equation that is even, normalized (`H 0 = 1`),
 369and monotone on `[0,∞)` is `H t = cosh (c · t)` for a single real `c`. The proof
 370uses no continuity, no smoothness, no Aczél package, and no least-upper-bound
 371axiom — only field operations, square roots, the order, and Archimedean density
 372(inside `monotone_additive_isLinear`). It therefore transfers verbatim to any
 373Archimedean real-closed field.
 374
 375Consequence for the δ program (the §9 question): the continuum is NOT required to
 376force the cost form. Monotonicity — an order property present on any ordered
 377field — does everything continuity was doing. The single residual `c` is exactly
 378the known unit-of-scale posit. So the framework's arbitrary content drops from
 379two nested posits (continuum + unit) to one (unit), and the continuum posit for
 380the cost dissolves. This is the positive resolution of the sharper §9 target. -/
 381theorem dAlembert_cosh_of_monotone {H : ℝ → ℝ}
 382    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
 383    (heven : Function.Even H) (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
 384    ∃ c : ℝ, ∀ t, H t = Real.cosh (c * t) := by
 385  have hφmul : ∀ a b, 0 ≤ a → 0 ≤ b →
 386      (H (a + b) + Real.sqrt ((H (a + b)) ^ 2 - 1))
 387        = (H a + Real.sqrt ((H a) ^ 2 - 1)) * (H b + Real.sqrt ((H b) ^ 2 - 1)) := by
 388    intro a b ha hb
 389    rcases le_total b a with hba | hab
 390    · exact phi_mul_of_monotone hd h0 hmono a b hb hba
 391    · have hp := phi_mul_of_monotone hd h0 hmono b a ha hab
 392      rw [add_comm b a] at hp
 393      rw [hp]; ring
 394  have hφpos : ∀ x, 0 ≤ x → (1 : ℝ) ≤ H x + Real.sqrt ((H x) ^ 2 - 1) := by
 395    intro x hx
 396    have h1 := dAlembert_ge_one_of_monotone h0 hmono x hx
 397    have h2 : 0 ≤ Real.sqrt ((H x) ^ 2 - 1) := Real.sqrt_nonneg _
 398    linarith
 399  have hφmono : MonotoneOn (fun x => Real.log (H x + Real.sqrt ((H x) ^ 2 - 1)))
 400      (Set.Ici (0 : ℝ)) := by
 401    intro x hx y hy hxy
 402    have hx0 := Set.mem_Ici.mp hx
 403    have hy0 := Set.mem_Ici.mp hy
 404    have hHxy : H x ≤ H y := hmono hx hy hxy
 405    have hge1x := dAlembert_ge_one_of_monotone h0 hmono x hx0
 406    have hsqle : Real.sqrt ((H x) ^ 2 - 1) ≤ Real.sqrt ((H y) ^ 2 - 1) :=
 407      Real.sqrt_le_sqrt (by nlinarith [hHxy, hge1x])
 408    show Real.log (H x + Real.sqrt ((H x) ^ 2 - 1))
 409        ≤ Real.log (H y + Real.sqrt ((H y) ^ 2 - 1))
 410    exact Real.log_le_log (by linarith [hφpos x hx0]) (by linarith)
 411  have hγadd : ∀ a b, 0 ≤ a → 0 ≤ b →
 412      Real.log (H (a + b) + Real.sqrt ((H (a + b)) ^ 2 - 1))
 413        = Real.log (H a + Real.sqrt ((H a) ^ 2 - 1))
 414          + Real.log (H b + Real.sqrt ((H b) ^ 2 - 1)) := by
 415    intro a b ha hb
 416    rw [hφmul a b ha hb]
 417    exact Real.log_mul (by have := hφpos a ha; linarith) (by have := hφpos b hb; linarith)
 418  have hγ0 : Real.log (H 0 + Real.sqrt ((H 0) ^ 2 - 1)) = 0 := by
 419    rw [h0]
 420    have h01 : (1 : ℝ) ^ 2 - 1 = 0 := by norm_num
 421    rw [h01, Real.sqrt_zero, add_zero, Real.log_one]
 422  have hlin := monotone_additive_nonneg_isLinear
 423    (f := fun x => Real.log (H x + Real.sqrt ((H x) ^ 2 - 1))) hγadd hφmono hγ0
 424  refine ⟨Real.log (H 1 + Real.sqrt ((H 1) ^ 2 - 1)), ?_⟩
 425  set c := Real.log (H 1 + Real.sqrt ((H 1) ^ 2 - 1)) with hc
 426  have hcosh_nonneg : ∀ t, 0 ≤ t → H t = Real.cosh (c * t) := by
 427    intro t ht
 428    have hge1t := dAlembert_ge_one_of_monotone h0 hmono t ht
 429    have hSt : 0 ≤ (H t) ^ 2 - 1 := by nlinarith [hge1t]
 430    have hφtpos : 0 < H t + Real.sqrt ((H t) ^ 2 - 1) := by linarith [hφpos t ht]
 431    have hloglin : Real.log (H t + Real.sqrt ((H t) ^ 2 - 1)) = c * t := hlin t ht
 432    have hφexp : H t + Real.sqrt ((H t) ^ 2 - 1) = Real.exp (c * t) := by
 433      rw [← hloglin]; exact (Real.exp_log hφtpos).symm
 434    have hsqsq : (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 = (H t) ^ 2 - 1 := Real.sq_sqrt hSt
 435    have hprod :
 436        (H t + Real.sqrt ((H t) ^ 2 - 1)) * (H t - Real.sqrt ((H t) ^ 2 - 1)) = 1 := by
 437      have hexp :
 438          (H t + Real.sqrt ((H t) ^ 2 - 1)) * (H t - Real.sqrt ((H t) ^ 2 - 1))
 439            = (H t) ^ 2 - (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 := by ring
 440      rw [hexp, hsqsq]; ring
 441    have hinv : H t - Real.sqrt ((H t) ^ 2 - 1) = (H t + Real.sqrt ((H t) ^ 2 - 1))⁻¹ :=
 442      eq_inv_of_mul_eq_one_right hprod
 443    have hHt : H t = (Real.exp (c * t) + (Real.exp (c * t))⁻¹) / 2 := by
 444      have e : H t
 445          = ((H t + Real.sqrt ((H t) ^ 2 - 1)) + (H t - Real.sqrt ((H t) ^ 2 - 1))) / 2 := by
 446        ring
 447      rw [e, hinv, hφexp]
 448    rw [hHt, Real.cosh_eq, Real.exp_neg]
 449  intro t
 450  rcases le_or_lt 0 t with ht | ht
 451  · exact hcosh_nonneg t ht
 452  · have hnt : H t = H (-t) := (heven t).symm
 453    rw [hnt, hcosh_nonneg (-t) (by linarith), show c * (-t) = -(c * t) by ring, Real.cosh_neg]
 454
 455/-- **§9 payoff: the cost FORM is forced by monotonicity alone (no continuity).**
 456
 457The cost function `F` (reciprocal-symmetric, normalized, satisfying the
 458composition law) is forced into the cosh log-shape `H_F t = cosh (c·t)` by the
 459single regularity hypothesis that `H_F = F∘exp + 1` is monotone on `[0,∞)`. This
 460is the completeness-free replacement for the `ContinuousOn`/Aczél-smoothness
 461hypothesis of `Cost.FunctionalEquation.law_of_logic_forces_jcost`: the composition
 462law gives the d'Alembert equation on `H_F`, reciprocal symmetry gives evenness,
 463normalization gives `H_F 0 = 1`, and `dAlembert_cosh_of_monotone` finishes using
 464only order + field + sqrt + Archimedean density. -/
 465theorem composition_law_monotone_forces_cosh_family (F : ℝ → ℝ)
 466    (hRecip : Cost.FunctionalEquation.IsReciprocalCost F)
 467    (hNorm : Cost.FunctionalEquation.IsNormalized F)
 468    (hComp : Cost.FunctionalEquation.SatisfiesCompositionLaw F)
 469    (hMono : MonotoneOn (Cost.FunctionalEquation.H F) (Set.Ici (0 : ℝ))) :
 470    ∃ c : ℝ, ∀ t, Cost.FunctionalEquation.H F t = Real.cosh (c * t) := by
 471  have hCoshAdd := (Cost.FunctionalEquation.composition_law_equiv_coshAdd F).mp hComp
 472  have h_direct := Cost.FunctionalEquation.CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
 473  have h_dAlembert : ∀ t u,
 474      Cost.FunctionalEquation.H F (t + u) + Cost.FunctionalEquation.H F (t - u)
 475        = 2 * Cost.FunctionalEquation.H F t * Cost.FunctionalEquation.H F u := by
 476    intro t u
 477    simp only [Cost.FunctionalEquation.H]
 478    linear_combination (h_direct t u)
 479  have h0 : Cost.FunctionalEquation.H F 0 = 1 := by
 480    simp only [Cost.FunctionalEquation.H]
 481    rw [Cost.FunctionalEquation.G_zero_of_unit F hNorm]; norm_num
 482  have heven : Function.Even (Cost.FunctionalEquation.H F) := by
 483    intro t
 484    simp only [Cost.FunctionalEquation.H]
 485    rw [Cost.FunctionalEquation.G_even_of_reciprocal_symmetry F (fun {x} hx => hRecip x hx) t]
 486  exact dAlembert_cosh_of_monotone h_dAlembert h0 heven hMono
 487
 488/-! ## The chain-facing entry point
 489
 490What the block above delivers is the cosh family. Turning that into `J` needs
 491one derivative computation and the observation that the calibration equation
 492`c² = 1` cannot tell `c = 1` from `c = -1`, which is harmless because `cosh` is
 493even. No completeness, no continuity, and no scale-family detour. -/
 494
 495/-- The log-coordinate curvature at the unit of the scaled cosh cost is `c²`.
 496
 497This is the calibration functional evaluated on the family the d'Alembert block
 498produces. It is the whole reason calibration can select a member: the map from
 499exponent to calibration value is `c ↦ c²`, so fixing the value to `1` fixes the
 500exponent up to sign. -/
 501theorem cosh_scale_curvature (l : ℝ) :
 502    deriv (deriv (fun t : ℝ => Real.cosh (l * t) - 1)) 0 = l ^ 2 := by
 503  have hlin : ∀ t : ℝ, HasDerivAt (fun t => l * t) l t := by
 504    intro t; simpa using (hasDerivAt_id t).const_mul l
 505  have hd1 : ∀ t : ℝ,
 506      HasDerivAt (fun t => Real.cosh (l * t) - 1) (Real.sinh (l * t) * l) t := by
 507    intro t; exact ((hlin t).cosh).sub_const 1
 508  have hderiv1 : deriv (fun t : ℝ => Real.cosh (l * t) - 1)
 509      = fun t => Real.sinh (l * t) * l := by
 510    funext t; exact (hd1 t).deriv
 511  have hd2 : HasDerivAt (fun t => Real.sinh (l * t) * l)
 512      (Real.cosh (l * 0) * l * l) 0 := ((hlin 0).sinh).mul_const l
 513  rw [hderiv1, hd2.deriv, mul_zero, Real.cosh_zero, one_mul]
 514  ring
 515
 516/-- In log coordinates `Cost.Jcost` is exactly `cosh`. -/
 517theorem H_jcost_eq_cosh (t : ℝ) :
 518    Cost.FunctionalEquation.H Cost.Jcost t = Real.cosh t := by
 519  simp only [Cost.FunctionalEquation.H, Cost.FunctionalEquation.G, Cost.Jcost,
 520    Real.cosh_eq, Real.exp_neg]
 521  ring
 522
 523/-- `cosh (l · t)` is nondecreasing on `[0, ∞)` whenever `l ≥ 0`. -/
 524theorem cosh_mul_monotoneOn {l : ℝ} (hl : 0 ≤ l) :
 525    MonotoneOn (fun t : ℝ => Real.cosh (l * t)) (Set.Ici (0 : ℝ)) := by
 526  intro a ha b hb hab
 527  have ha0 : (0 : ℝ) ≤ a := Set.mem_Ici.mp ha
 528  have hb0 : (0 : ℝ) ≤ b := Set.mem_Ici.mp hb
 529  refine Real.cosh_le_cosh.mpr ?_
 530  rw [abs_of_nonneg (mul_nonneg hl ha0), abs_of_nonneg (mul_nonneg hl hb0)]
 531  exact mul_le_mul_of_nonneg_left hab hl
 532
 533/-- `J` satisfies the order hypothesis. Without this the order route would be a
 534theorem about an empty class, so it is the non-vacuity witness for everything
 535the chain now hangs on `MonotoneOn`. -/
 536theorem H_jcost_monotoneOn :
 537    MonotoneOn (Cost.FunctionalEquation.H Cost.Jcost) (Set.Ici (0 : ℝ)) := by
 538  have h : Cost.FunctionalEquation.H Cost.Jcost = fun t : ℝ => Real.cosh (1 * t) := by
 539    funext t; rw [H_jcost_eq_cosh, one_mul]
 540  rw [h]
 541  exact cosh_mul_monotoneOn (by norm_num)
 542
 543/-- **The recognition cost is forced by order.**
 544
 545A reciprocal-symmetric, normalized, composition-law cost whose log transform is
 546nondecreasing on `[0, ∞)` and which meets the unit calibration equals
 547`Cost.Jcost` on the positives. Continuity is never invoked, no smoothness
 548package is required, and nothing in the proof needs a least upper bound, so the
 549statement is available on any Archimedean ordered field.
 550
 551This is the theorem the forcing chain's T5 rung now cites. The older route
 552through the scale family, `law_of_logic_forces_jcost_monotone`, proves the same
 553thing and stays where it is; it just cannot be named from below the completion
 554layer, which is what this version fixes. -/
 555theorem jcost_forced_by_order (F : ℝ → ℝ)
 556    (hRecip : Cost.FunctionalEquation.IsReciprocalCost F)
 557    (hNorm : Cost.FunctionalEquation.IsNormalized F)
 558    (hComp : Cost.FunctionalEquation.SatisfiesCompositionLaw F)
 559    (hMono : MonotoneOn (Cost.FunctionalEquation.H F) (Set.Ici (0 : ℝ)))
 560    (hCalib : Cost.FunctionalEquation.IsCalibrated F) :
 561    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 562  obtain ⟨c, hc⟩ :=
 563    composition_law_monotone_forces_cosh_family F hRecip hNorm hComp hMono
 564  have hGpt : ∀ t : ℝ,
 565      Cost.FunctionalEquation.G F t = Real.cosh (c * t) - 1 := by
 566    intro t
 567    have ht := hc t
 568    simp only [Cost.FunctionalEquation.H] at ht
 569    linarith
 570  have hG : Cost.FunctionalEquation.G F = fun t : ℝ => Real.cosh (c * t) - 1 :=
 571    funext hGpt
 572  have hc2 : c ^ 2 = 1 := by
 573    have hcal : deriv (deriv (Cost.FunctionalEquation.G F)) 0 = 1 := hCalib
 574    rw [hG, cosh_scale_curvature c] at hcal
 575    exact hcal
 576  -- `c² = 1` leaves the sign free, and `cosh` cannot see it.
 577  have hcosh_eq : ∀ t : ℝ, Real.cosh (c * t) = Real.cosh t := by
 578    intro t
 579    have hfac : (c - 1) * (c + 1) = 0 := by nlinarith [hc2]
 580    rcases mul_eq_zero.mp hfac with h | h
 581    · rw [show c = 1 by linarith, one_mul]
 582    · rw [show c = -1 by linarith, show (-1 : ℝ) * t = -t by ring, Real.cosh_neg]
 583  intro x hx
 584  have hgx : Cost.FunctionalEquation.G F (Real.log x) = F x := by
 585    simp only [Cost.FunctionalEquation.G]
 586    rw [Real.exp_log hx]
 587  have hval : F x = Real.cosh (Real.log x) - 1 := by
 588    have h1 := hGpt (Real.log x)
 589    rw [hgx, hcosh_eq] at h1
 590    exact h1
 591  rw [hval, Cost.Jcost, Real.cosh_eq, Real.exp_log hx, Real.exp_neg, Real.exp_log hx]
 592
 593/-! ## Axiom audit -/
 594
 595#print axioms cosh_scale_curvature
 596#print axioms H_jcost_monotoneOn
 597#print axioms jcost_forced_by_order
 598
 599end PRCJCost
 600end PrimitiveRecognitionCalculus
 601end Foundation
 602end IndisputableMonolith
 603