Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcmonotone Dalembert D Alembert S Add

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Prcmonotone Dalembert D Alembert S Add

A single equation for the square-root part of a d'Alembert solution, proved with order alone and no reliance on continuity.

Verify this page

The addition formula

In the classical theory of functional equations, the d'Alembert equation H(s+t) + H(s−t) = 2 H(s) H(t) is the defining relation for the hyperbolic cosine. Its solutions include cosh(a t) and cos(a t). The declaration dAlembert_S_add_of_monotone proves a companion identity for the quantity S(t) = √(H(t)² − 1), which plays the role of the hyperbolic sine. For 0 ≤ t ≤ s, it states that S(s+t) = H(s) S(t) + S(s) H(t). This is the addition formula for sinh, derived from the d'Alembert equation, the normalization H(0) = 1, and the assumption that H is nondecreasing on the nonnegative reals.

The proof is purely algebraic and order-theoretic. It uses the earlier sign-fixed difference identity and the H-addition formula, both of which follow from the d'Alembert equation and monotonicity. No continuity, no smoothness, no least-upper-bound axiom, and no analytic regularity package is invoked. The monotonicity assumption does the work that continuity usually performs: it fixes the sign of the square root in the difference formula, selecting the cosh branch over the cosine branch. The theorem is therefore available on any Archimedean ordered field, not just the real numbers with their completeness property.

This identity is a load-bearing brick in a larger derivation. Together with the H-addition formula, it packages into a multiplicative law for φ(x) = H(x) + √(H(x)² − 1), namely φ(s+t) = φ(s) φ(t). Since φ is positive and monotone, its logarithm is an additive monotone function, which a separate theorem forces to be linear. This yields H(t) = cosh(c t) for some real c, with no completeness assumption. The framework's library then uses this to show that a reciprocal-symmetric, normalized, composition-law cost whose log transform is monotone is forced to equal the J-cost function.

The declaration does not itself state the final cosh form. It only establishes the addition formula for S. The step from this identity to the full classification of H as cosh of a linear function is a separate theorem in the same block. The declaration also does not claim that the d'Alembert equation alone, without monotonicity, forces the cosh form; the cosine branch H(t) = cos(c t) is a genuine solution without that order assumption. The monotonicity hypothesis is essential to exclude it.

THEOREM dAlembert_S_add_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
dAlembert_S_add_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:316 
/-- **`S`-addition identity (monotone-fixed).** With `S x = √(H x²−1)`, for
`0 ≤ t ≤ s` the "sinh" addition formula `S(s+t) = H s · S t + S s · H t` holds.
Proved by squaring (using the `H`-addition formula) and taking nonnegative roots.
Completeness-free. -/
theorem dAlembert_S_add_of_monotone {H : ℝ → ℝ}
    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
    (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
    ∀ s t, 0 ≤ t → t ≤ s →
      Real.sqrt ((H (s + t)) ^ 2 - 1)
        = H s * Real.sqrt ((H t) ^ 2 - 1) + Real.sqrt ((H s) ^ 2 - 1) * H t := by
  intro s t ht hts
  have hge1s : 1 ≤ H s := dAlembert_ge_one_of_monotone h0 hmono s (le_trans ht hts)
  have hge1t : 1 ≤ H t := dAlembert_ge_one_of_monotone h0 hmono t ht
  have hHs0 : 0 ≤ H s := by linarith
  have hHt0 : 0 ≤ H t := by linarith
  have hSs : 0 ≤ (H s) ^ 2 - 1 := by nlinarith [hge1s]
  have hSt : 0 ≤ (H t) ^ 2 - 1 := by nlinarith [hge1t]
  have hadd := dAlembert_add_of_monotone hd h0 hmono s t ht hts
  have hu := Real.sq_sqrt hSs
  have hv := Real.sq_sqrt hSt
  have hrhs_nonneg :
      0 ≤ H s * Real.sqrt ((H t) ^ 2 - 1) + Real.sqrt ((H s) ^ 2 - 1) * H t := by
    have t1 : 0 ≤ H s * Real.sqrt ((H t) ^ 2 - 1) := mul_nonneg hHs0 (Real.sqrt_nonneg _)
    have t2 : 0 ≤ Real.sqrt ((H s) ^ 2 - 1) * H t := mul_nonneg (Real.sqrt_nonneg _) hHt0
    linarith
  have rhs_sq :
      (H s * Real.sqrt ((H t) ^ 2 - 1) + Real.sqrt ((H s) ^ 2 - 1) * H t) ^ 2
        = (H (s + t)) ^ 2 - 1 := by
    rw [hadd]
    linear_combination ((H t) ^ 2 - (Real.sqrt ((H t) ^ 2 - 1)) ^ 2) * hu + hv
  rw [← rhs_sq]
  exact Real.sqrt_sq hrhs_nonneg
THEOREM dAlembert_S_add_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
dAlembert_S_add_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:316 
/-- **`S`-addition identity (monotone-fixed).** With `S x = √(H x²−1)`, for
`0 ≤ t ≤ s` the "sinh" addition formula `S(s+t) = H s · S t + S s · H t` holds.
Proved by squaring (using the `H`-addition formula) and taking nonnegative roots.
Completeness-free. -/
theorem dAlembert_S_add_of_monotone {H : ℝ → ℝ}
    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
    (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
    ∀ s t, 0 ≤ t → t ≤ s →
      Real.sqrt ((H (s + t)) ^ 2 - 1)
        = H s * Real.sqrt ((H t) ^ 2 - 1) + Real.sqrt ((H s) ^ 2 - 1) * H t := by
  intro s t ht hts
  have hge1s : 1 ≤ H s := dAlembert_ge_one_of_monotone h0 hmono s (le_trans ht hts)
  have hge1t : 1 ≤ H t := dAlembert_ge_one_of_monotone h0 hmono t ht
  have hHs0 : 0 ≤ H s := by linarith
  have hHt0 : 0 ≤ H t := by linarith
  have hSs : 0 ≤ (H s) ^ 2 - 1 := by nlinarith [hge1s]
  have hSt : 0 ≤ (H t) ^ 2 - 1 := by nlinarith [hge1t]
  have hadd := dAlembert_add_of_monotone hd h0 hmono s t ht hts
  have hu := Real.sq_sqrt hSs
  have hv := Real.sq_sqrt hSt
  have hrhs_nonneg :
      0 ≤ H s * Real.sqrt ((H t) ^ 2 - 1) + Real.sqrt ((H s) ^ 2 - 1) * H t := by
    have t1 : 0 ≤ H s * Real.sqrt ((H t) ^ 2 - 1) := mul_nonneg hHs0 (Real.sqrt_nonneg _)
    have t2 : 0 ≤ Real.sqrt ((H s) ^ 2 - 1) * H t := mul_nonneg (Real.sqrt_nonneg _) hHt0
    linarith
  have rhs_sq :
      (H s * Real.sqrt ((H t) ^ 2 - 1) + Real.sqrt ((H s) ^ 2 - 1) * H t) ^ 2
        = (H (s + t)) ^ 2 - 1 := by
    rw [hadd]
    linear_combination ((H t) ^ 2 - (Real.sqrt ((H t) ^ 2 - 1)) ^ 2) * hu + hv
  rw [← rhs_sq]
  exact Real.sqrt_sq hrhs_nonneg
THEOREM dAlembert_diff_eq_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
dAlembert_diff_eq_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:251 
/-- **§9 sign crux, RESOLVED: monotonicity fixes the sign.** For `0 ≤ t ≤ s`,
both `s+t` and `s−t` lie in `[0,∞)`, so monotonicity of `H` there forces
`H(s+t) ≥ H(s−t)`; the difference is the NONNEGATIVE root of the square computed
in `dAlembert_diff_sq`:

`H(s+t) − H(s−t) = 2 √(H(s)²−1) · √(H(t)²−1)`.

This is the cosh addition formula `cosh(a+b) − cosh(a−b) = 2 sinh a sinh b` with
`sinh = √(cosh²−1) ≥ 0`. The sign — the one place the analytic proof used
continuity — is here pinned by ORDER ALONE. So the answer to the §9 sub-question
"can monotonicity fix the sign?" is YES. Completeness is not needed for this
step; only the order structure of the field is. -/
theorem dAlembert_diff_eq_of_monotone {H : ℝ → ℝ}
    (hd : ∀ s t, H (s + t) + H (s - t) = 2 * H s * H t) (h0 : H 0 = 1)
    (hmono : MonotoneOn H (Set.Ici (0 : ℝ))) :
    ∀ s t, 0 ≤ t → t ≤ s →
      H (s + t) - H (s - t)
        = 2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1) := by
  intro s t ht hts
  have hs0 : 0 ≤ s := le_trans ht hts
  have hge1s : 1 ≤ H s := dAlembert_ge_one_of_monotone h0 hmono s hs0
  have hge1t : 1 ≤ H t := dAlembert_ge_one_of_monotone h0 hmono t ht
  have hSs : 0 ≤ (H s) ^ 2 - 1 := by nlinarith [hge1s]
  have hSt : 0 ≤ (H t) ^ 2 - 1 := by nlinarith [hge1t]
  have hsmt_nonneg : 0 ≤ s - t := by linarith
  have hspt_nonneg : 0 ≤ s + t := by linarith
  have hdiff_nonneg : 0 ≤ H (s + t) - H (s - t) := by
    have hle : H (s - t) ≤ H (s + t) :=
      hmono (Set.mem_Ici.mpr hsmt_nonneg) (Set.mem_Ici.mpr hspt_nonneg) (by linarith)
    linarith
  have hrhs_nonneg :
      0 ≤ 2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1) := by positivity
  have hsq := dAlembert_diff_sq hd h0 s t
  have hrhs_sq :
      (2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1)) ^ 2
        = 4 * ((H s) ^ 2 - 1) * ((H t) ^ 2 - 1) := by
    rw [show (2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1)) ^ 2
          = 4 * (Real.sqrt ((H s) ^ 2 - 1)) ^ 2 * (Real.sqrt ((H t) ^ 2 - 1)) ^ 2 by ring,
       Real.sq_sqrt hSs, Real.sq_sqrt hSt]
  have hsquares :
      (H (s + t) - H (s - t)) ^ 2
        = (2 * Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1)) ^ 2 := by
    rw [hsq, hrhs_sq]
  have hsqrt := congrArg Real.sqrt hsquares
  rwa [Real.sqrt_sq hdiff_nonneg, Real.sqrt_sq hrhs_nonneg] at hsqrt

What this page does not claim

The declaration does not state the final classification H(t) = cosh(c t); that is a separate theorem. The declaration does not apply to d'Alembert solutions that are not monotone on the nonnegative reals. The declaration does not claim that the d'Alembert equation alone forces the cosh form.

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