Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcmonotone Dalembert Monotone Additiv

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Prcmonotone Dalembert Monotone Additiv

A single, simple assumption about a function's shape, monotonicity, replaces the heavy analytic machinery of continuity in forcing a linear form.

Verify this page

Order replaces continuity

In mathematics, a function is additive if it preserves addition: the value at a sum equals the sum of the values. The classic question is whether an additive function must be linear, meaning it looks like a straight line through the origin. The answer is no in general, but yes if the function is also monotone, meaning it never decreases as its input increases. The theorem monotone_additive_nonneg_isLinear states this for functions defined on the nonnegative real numbers: if such a function is additive for nonnegative inputs, monotone on that domain, and maps zero to zero, then it is exactly f t = f 1 * t for all nonnegative t.

The classical result, often attributed to Cauchy, requires continuity to force linearity. This theorem shows that monotonicity alone, a purely order-theoretic property, is enough. The proof uses only the density of rational numbers in an Archimedean ordered field, not the least-upper-bound axiom. This means the statement holds in any such field, not just the real numbers with their completeness property.

In Recognition Science, this result is a load-bearing brick. The framework's central cost function is derived from a d'Alembert equation, and its solution is shown to be a hyperbolic cosine composed with a linear map. The linear map is exactly what this theorem forces, using monotonicity instead of continuity. This removes the need for the continuum as a hypothesis: the cost form is forced by order alone, with only a single unit of scale remaining as an arbitrary choice.

The theorem does not claim that all additive functions are linear, only those that are monotone. It does not apply to functions that are merely additive on the whole real line without the monotonicity condition, where pathological solutions exist. It also does not claim anything about the value of the slope f 1; that remains a free parameter, the unit of scale.

THEOREM monotone_additive_nonneg_isLinear · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
monotone_additive_nonneg_isLinear · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:119 
/-- **Nonnegative version: additive-on-`[0,∞)` + monotone ⇒ linear on `[0,∞)`.**
A function additive for nonnegative arguments and monotone on `[0,∞)` with
`f 0 = 0` satisfies `f t = f 1 · t` for `t ≥ 0`. Proved by the odd extension to
all of `ℝ` plus `monotone_additive_isLinear`; completeness-free. This is the form
the `log∘φ` exponent of the d'Alembert/monotone route actually has (additivity
only comes from `φ(s+t)=φ(s)φ(t)` for nonnegative `s,t`). -/
theorem monotone_additive_nonneg_isLinear {f : ℝ → ℝ}
    (hadd : ∀ a b, 0 ≤ a → 0 ≤ b → f (a + b) = f a + f b)
    (hmono : MonotoneOn f (Set.Ici (0 : ℝ))) (hf0 : f 0 = 0) :
    ∀ t, 0 ≤ t → f t = f 1 * t := by
  classical
  have hsub : ∀ a b, 0 ≤ b → b ≤ a → f (a - b) = f a - f b := by
    intro a b hb hba
    have h := hadd (a - b) b (by linarith) hb
    rw [sub_add_cancel] at h
    linarith
  set g : ℝ → ℝ := fun t => if 0 ≤ t then f t else - f (-t) with hg
  have hg_pos : ∀ t, 0 ≤ t → g t = f t := by intro t ht; simp [hg, ht]
  have hg_neg : ∀ t, t < 0 → g t = - f (-t) := by
    intro t ht; simp [hg, not_le.mpr ht]
  have hgadd : ∀ s t, g (s + t) = g s + g t := by
    intro s t
    rcases le_or_lt 0 s with hs | hs <;> rcases le_or_lt 0 t with ht | ht
    · rw [hg_pos s hs, hg_pos t ht, hg_pos (s + t) (by linarith), hadd s t hs ht]
    · rw [hg_pos s hs, hg_neg t ht]
      rcases le_or_lt 0 (s + t) with hst | hst
      · rw [hg_pos (s + t) hst]
        have hh := hsub s (-t) (by linarith) (by linarith)
        rw [sub_neg_eq_add] at hh
        rw [hh]; ring
      · rw [hg_neg (s + t) hst]
        have hh := hsub (-t) s (by linarith) (by linarith)
        rw [show -t - s = -(s + t) by ring] at hh
        rw [hh]; ring
    · rw [hg_neg s hs, hg_pos t ht]
      rcases le_or_lt 0 (s + t) with hst | hst
      · rw [hg_pos (s + t) hst]
        have hh := hsub t (-s) (by linarith) (by linarith)
        rw [show t - -s = s + t by ring] at hh
        rw [hh]; ring
      · rw [hg_neg (s + t) hst]
        have hh := hsub (-s) t (by linarith) (by linarith)
        rw [show -s - t = -(s + t) by ring] at hh
        rw [hh]; ring
    · rw [hg_neg s hs, hg_neg t ht, hg_neg (s + t) (by linarith),
        show -(s + t) = (-s) + (-t) by ring, hadd (-s) (-t) (by linarith) (by linarith)]
      ring
  have hgmono : Monotone g := by
    intro x y hxy
    rcases le_or_lt 0 x with hx | hx
    · have hy : 0 ≤ y := le_trans hx hxy
      rw [hg_pos x hx, hg_pos y hy]
      exact hmono (Set.mem_Ici.mpr hx) (Set.mem_Ici.mpr hy) hxy
    · rcases le_or_lt 0 y with hy | hy
      · rw [hg_neg x hx, hg_pos y hy]
        have hfnx : f 0 ≤ f (-x) :=
          hmono (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr (by linarith)) (by linarith)
        have hfy : f 0 ≤ f y :=
          hmono (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr hy) hy
        rw [hf0] at hfnx hfy
        linarith
      · rw [hg_neg x hx, hg_neg y hy]
        have hle : f (-y) ≤ f (-x) :=
          hmono (Set.mem_Ici.mpr (by linarith)) (Set.mem_Ici.mpr (by linarith)) (by linarith)
        linarith
  have hlin := monotone_additive_isLinear hgadd hgmono
  have hg1 : g 1 = f 1 := hg_pos 1 (by norm_num)
  intro t ht
  have hlt := hlin t
  rw [hg_pos t ht, hg1] at hlt
  exact hlt
THEOREM monotone_additive_nonneg_isLinear · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
monotone_additive_nonneg_isLinear · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:119 
/-- **Nonnegative version: additive-on-`[0,∞)` + monotone ⇒ linear on `[0,∞)`.**
A function additive for nonnegative arguments and monotone on `[0,∞)` with
`f 0 = 0` satisfies `f t = f 1 · t` for `t ≥ 0`. Proved by the odd extension to
all of `ℝ` plus `monotone_additive_isLinear`; completeness-free. This is the form
the `log∘φ` exponent of the d'Alembert/monotone route actually has (additivity
only comes from `φ(s+t)=φ(s)φ(t)` for nonnegative `s,t`). -/
theorem monotone_additive_nonneg_isLinear {f : ℝ → ℝ}
    (hadd : ∀ a b, 0 ≤ a → 0 ≤ b → f (a + b) = f a + f b)
    (hmono : MonotoneOn f (Set.Ici (0 : ℝ))) (hf0 : f 0 = 0) :
    ∀ t, 0 ≤ t → f t = f 1 * t := by
  classical
  have hsub : ∀ a b, 0 ≤ b → b ≤ a → f (a - b) = f a - f b := by
    intro a b hb hba
    have h := hadd (a - b) b (by linarith) hb
    rw [sub_add_cancel] at h
    linarith
  set g : ℝ → ℝ := fun t => if 0 ≤ t then f t else - f (-t) with hg
  have hg_pos : ∀ t, 0 ≤ t → g t = f t := by intro t ht; simp [hg, ht]
  have hg_neg : ∀ t, t < 0 → g t = - f (-t) := by
    intro t ht; simp [hg, not_le.mpr ht]
  have hgadd : ∀ s t, g (s + t) = g s + g t := by
    intro s t
    rcases le_or_lt 0 s with hs | hs <;> rcases le_or_lt 0 t with ht | ht
    · rw [hg_pos s hs, hg_pos t ht, hg_pos (s + t) (by linarith), hadd s t hs ht]
    · rw [hg_pos s hs, hg_neg t ht]
      rcases le_or_lt 0 (s + t) with hst | hst
      · rw [hg_pos (s + t) hst]
        have hh := hsub s (-t) (by linarith) (by linarith)
        rw [sub_neg_eq_add] at hh
        rw [hh]; ring
      · rw [hg_neg (s + t) hst]
        have hh := hsub (-t) s (by linarith) (by linarith)
        rw [show -t - s = -(s + t) by ring] at hh
        rw [hh]; ring
    · rw [hg_neg s hs, hg_pos t ht]
      rcases le_or_lt 0 (s + t) with hst | hst
      · rw [hg_pos (s + t) hst]
        have hh := hsub t (-s) (by linarith) (by linarith)
        rw [show t - -s = s + t by ring] at hh
        rw [hh]; ring
      · rw [hg_neg (s + t) hst]
        have hh := hsub (-s) t (by linarith) (by linarith)
        rw [show -s - t = -(s + t) by ring] at hh
        rw [hh]; ring
    · rw [hg_neg s hs, hg_neg t ht, hg_neg (s + t) (by linarith),
        show -(s + t) = (-s) + (-t) by ring, hadd (-s) (-t) (by linarith) (by linarith)]
      ring
  have hgmono : Monotone g := by
    intro x y hxy
    rcases le_or_lt 0 x with hx | hx
    · have hy : 0 ≤ y := le_trans hx hxy
      rw [hg_pos x hx, hg_pos y hy]
      exact hmono (Set.mem_Ici.mpr hx) (Set.mem_Ici.mpr hy) hxy
    · rcases le_or_lt 0 y with hy | hy
      · rw [hg_neg x hx, hg_pos y hy]
        have hfnx : f 0 ≤ f (-x) :=
          hmono (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr (by linarith)) (by linarith)
        have hfy : f 0 ≤ f y :=
          hmono (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr hy) hy
        rw [hf0] at hfnx hfy
        linarith
      · rw [hg_neg x hx, hg_neg y hy]
        have hle : f (-y) ≤ f (-x) :=
          hmono (Set.mem_Ici.mpr (by linarith)) (Set.mem_Ici.mpr (by linarith)) (by linarith)
        linarith
  have hlin := monotone_additive_isLinear hgadd hgmono
  have hg1 : g 1 = f 1 := hg_pos 1 (by norm_num)
  intro t ht
  have hlt := hlin t
  rw [hg_pos t ht, hg1] at hlt
  exact hlt
THEOREM dAlembert_cosh_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
dAlembert_cosh_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:366 
/-- **§9 RESOLVED, POSITIVE: the cosh cost form is forced WITHOUT completeness.**

A solution `H` of the d'Alembert equation that is even, normalized (`H 0 = 1`),
and monotone on `[0,∞)` is `H t = cosh (c · t)` for a single real `c`. The proof
uses no continuity, no smoothness, no Aczél package, and no least-upper-bound
axiom — only field operations, square roots, the order, and Archimedean density
(inside `monotone_additive_isLinear`). It therefore transfers verbatim to any
Archimedean real-closed field.

Consequence for the δ program (the §9 question): the continuum is NOT required to
force the cost form. Monotonicity — an order property present on any ordered
field — does everything continuity was doing. The single residual `c` is exactly
the known unit-of-scale posit. So the framework's arbitrary content drops from
two nested posits (continuum + unit) to one (unit), and the continuum posit for
the cost dissolves. This is the positive resolution of the sharper §9 target. -/
theorem dAlembert_cosh_of_monotone {H : ℝ → ℝ}
    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
    (heven : Function.Even H) (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
    ∃ c : ℝ, ∀ t, H t = Real.cosh (c * t) := by
  have hφmul : ∀ a b, 0 ≤ a → 0 ≤ b →
      (H (a + b) + Real.sqrt ((H (a + b)) ^ 2 - 1))
        = (H a + Real.sqrt ((H a) ^ 2 - 1)) * (H b + Real.sqrt ((H b) ^ 2 - 1)) := by
    intro a b ha hb
    rcases le_total b a with hba | hab
    · exact phi_mul_of_monotone hd h0 hmono a b hb hba
    · have hp := phi_mul_of_monotone hd h0 hmono b a ha hab
      rw [add_comm b a] at hp
      rw [hp]; ring
  have hφpos : ∀ x, 0 ≤ x → (1 : ℝ) ≤ H x + Real.sqrt ((H x) ^ 2 - 1) := by
    intro x hx
    have h1 := dAlembert_ge_one_of_monotone h0 hmono x hx
    have h2 : 0 ≤ Real.sqrt ((H x) ^ 2 - 1) := Real.sqrt_nonneg _
    linarith
  have hφmono : MonotoneOn (fun x => Real.log (H x + Real.sqrt ((H x) ^ 2 - 1)))
      (Set.Ici (0 : ℝ)) := by
    intro x hx y hy hxy
    have hx0 := Set.mem_Ici.mp hx
    have hy0 := Set.mem_Ici.mp hy
    have hHxy : H x ≤ H y := hmono hx hy hxy
    have hge1x := dAlembert_ge_one_of_monotone h0 hmono x hx0
    have hsqle : Real.sqrt ((H x) ^ 2 - 1) ≤ Real.sqrt ((H y) ^ 2 - 1) :=
      Real.sqrt_le_sqrt (by nlinarith [hHxy, hge1x])
    show Real.log (H x + Real.sqrt ((H x) ^ 2 - 1))
        ≤ Real.log (H y + Real.sqrt ((H y) ^ 2 - 1))
    exact Real.log_le_log (by linarith [hφpos x hx0]) (by linarith)
  have hγadd : ∀ a b, 0 ≤ a → 0 ≤ b →
      Real.log (H (a + b) + Real.sqrt ((H (a + b)) ^ 2 - 1))
        = Real.log (H a + Real.sqrt ((H a) ^ 2 - 1))
          + Real.log (H b + Real.sqrt ((H b) ^ 2 - 1)) := by
    intro a b ha hb
    rw [hφmul a b ha hb]
    exact Real.log_mul (by have := hφpos a ha; linarith) (by have := hφpos b hb; linarith)
  have hγ0 : Real.log (H 0 + Real.sqrt ((H 0) ^ 2 - 1)) = 0 := by
    rw [h0]
    have h01 : (1 : ℝ) ^ 2 - 1 = 0 := by norm_num
    rw [h01, Real.sqrt_zero, add_zero, Real.log_one]
  have hlin := monotone_additive_nonneg_isLinear
    (f := fun x => Real.log (H x + Real.sqrt ((H x) ^ 2 - 1))) hγadd hφmono hγ0
  refine ⟨Real.log (H 1 + Real.sqrt ((H 1) ^ 2 - 1)), ?_⟩
  set c := Real.log (H 1 + Real.sqrt ((H 1) ^ 2 - 1)) with hc
  have hcosh_nonneg : ∀ t, 0 ≤ t → H t = Real.cosh (c * t) := by
    intro t ht
    have hge1t := dAlembert_ge_one_of_monotone h0 hmono t ht
    have hSt : 0 ≤ (H t) ^ 2 - 1 := by nlinarith [hge1t]
    have hφtpos : 0 < H t + Real.sqrt ((H t) ^ 2 - 1) := by linarith [hφpos t ht]
    have hloglin : Real.log (H t + Real.sqrt ((H t) ^ 2 - 1)) = c * t := hlin t ht
    have hφexp : H t + Real.sqrt ((H t) ^ 2 - 1) = Real.exp (c * t) := by
      rw [← hloglin]; exact (Real.exp_log hφtpos).symm
    have hsqsq : (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 = (H t) ^ 2 - 1 := Real.sq_sqrt hSt
    have hprod :
        (H t + Real.sqrt ((H t) ^ 2 - 1)) * (H t - Real.sqrt ((H t) ^ 2 - 1)) = 1 := by
      have hexp :
          (H t + Real.sqrt ((H t) ^ 2 - 1)) * (H t - Real.sqrt ((H t) ^ 2 - 1))
            = (H t) ^ 2 - (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 := by ring
      rw [hexp, hsqsq]; ring
    have hinv : H t - Real.sqrt ((H t) ^ 2 - 1) = (H t + Real.sqrt ((H t) ^ 2 - 1))⁻¹ :=
      eq_inv_of_mul_eq_one_right hprod
    have hHt : H t = (Real.exp (c * t) + (Real.exp (c * t))⁻¹) / 2 := by
      have e : H t
          = ((H t + Real.sqrt ((H t) ^ 2 - 1)) + (H t - Real.sqrt ((H t) ^ 2 - 1))) / 2 := by
        ring
      rw [e, hinv, hφexp]
    rw [hHt, Real.cosh_eq, Real.exp_neg]
  intro t
  rcases le_or_lt 0 t with ht | ht
  · exact hcosh_nonneg t ht
  · have hnt : H t = H (-t) := (heven t).symm
    rw [hnt, hcosh_nonneg (-t) (by linarith), show c * (-t) = -(c * t) by ring, Real.cosh_neg]

What this page does not claim

This theorem does not claim that all additive functions are linear, only those that are monotone. It does not apply to functions that are merely additive on the whole real line without the monotonicity condition. It does not claim anything about the value of the slope f 1; that remains a free parameter.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND