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

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Prcmonotone Dalembert D Alembert Add O

A single order property, monotonicity, replaces continuity in forcing the shape of a fundamental cost function.

Verify this page

The addition formula

The declaration dAlembert_add_of_monotone establishes a precise algebraic identity for functions that satisfy the d'Alembert equation, a classical functional equation of the form H(s+t) + H(s−t) = 2 H(s) H(t), with the normalization H(0) = 1. The theorem states that if such a function H is monotone, meaning nondecreasing, on the nonnegative real numbers, then for any 0 ≤ t ≤ s, the value at a sum decomposes as H(s+t) = H(s) H(t) + √(H(s)² − 1) · √(H(t)² − 1). This is the addition formula for the hyperbolic cosine, written in terms of H and its associated square-root function.

The classical context matters. The d'Alembert equation was studied by Jean le Rond d'Alembert in the 1740s in work on vibrating strings, and its solutions include both the hyperbolic cosine and the ordinary cosine families. The formula above is the cosh addition law: cosh(a+b) = cosh(a) cosh(b) + sinh(a) sinh(b), where the square root term plays the role of sinh. What the theorem adds is a regularity condition. Without any regularity assumption, the d'Alembert equation admits pathological solutions. The standard analytic hypothesis that selects the nice solutions is continuity. This declaration shows that monotonicity, a purely order-theoretic property available on any ordered field, suffices in its place.

The proof is short and purely algebraic once the sign is fixed. The d'Alembert equation gives the sum law for H(s+t) + H(s−t). A companion result, dAlembert_diff_eq_of_monotone, uses monotonicity to fix the sign of the difference H(s+t) − H(s−t) as the nonnegative square root. Adding the sum and difference laws and dividing by two yields the addition formula. The argument uses only field operations, square roots, and the order structure; it never invokes continuity, smoothness, or the least-upper-bound axiom.

In Recognition Science, this declaration is a load-bearing brick in a larger chain. The framework's central cost function J(x) = (x + 1/x)/2 − 1 satisfies the d'Alembert equation after a logarithmic change of variables. The classical uniqueness theorem for J used continuity as a regularity hypothesis. The monotone route replaces that analytic input with an order-theoretic one, showing that the continuum is not required to force the cost form. The single residual freedom is a scale parameter c, which calibration later fixes to 1. The declaration does not claim that monotonicity is necessary, only sufficient, and it does not by itself identify which member of the cosh family is selected.

THEOREM dAlembert_add_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
dAlembert_add_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:297 
/-- **Cosh addition formula, monotone-fixed sign.** For `0 ≤ t ≤ s`,
`H(s+t) = H s · H t + √(H s²−1)·√(H t²−1)`, the half-sum of the sum law and the
sign-fixed difference law. Completeness-free. This is the multiplicative seed:
with `φ(x) = H x + √(H x²−1)`, this and the matching `S`-addition identity give
`φ(s+t) = φ(s)·φ(t)`, i.e. `log ∘ φ` is additive — and monotone, hence linear by
`monotone_additive_isLinear`, hence `H = cosh(linear)` with no completeness. -/
theorem dAlembert_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 →
      H (s + t)
        = H s * H t + Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1) := by
  intro s t ht hts
  have hsum := hd s t
  have hdiff := dAlembert_diff_eq_of_monotone hd h0 hmono s t ht hts
  have e : 2 * H (s + t) = (H (s + t) + H (s - t)) + (H (s + t) - H (s - t)) := by ring
  rw [hsum, hdiff] at e
  linear_combination e / 2
THEOREM dAlembert_add_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean
dAlembert_add_of_monotone · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCMonotoneDAlembert.lean:297 
/-- **Cosh addition formula, monotone-fixed sign.** For `0 ≤ t ≤ s`,
`H(s+t) = H s · H t + √(H s²−1)·√(H t²−1)`, the half-sum of the sum law and the
sign-fixed difference law. Completeness-free. This is the multiplicative seed:
with `φ(x) = H x + √(H x²−1)`, this and the matching `S`-addition identity give
`φ(s+t) = φ(s)·φ(t)`, i.e. `log ∘ φ` is additive — and monotone, hence linear by
`monotone_additive_isLinear`, hence `H = cosh(linear)` with no completeness. -/
theorem dAlembert_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 →
      H (s + t)
        = H s * H t + Real.sqrt ((H s) ^ 2 - 1) * Real.sqrt ((H t) ^ 2 - 1) := by
  intro s t ht hts
  have hsum := hd s t
  have hdiff := dAlembert_diff_eq_of_monotone hd h0 hmono s t ht hts
  have e : 2 * H (s + t) = (H (s + t) + H (s - t)) + (H (s + t) - H (s - t)) := by ring
  rw [hsum, hdiff] at e
  linear_combination e / 2
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 claim that monotonicity is necessary for the addition formula, only that it is sufficient. The declaration does not by itself identify which member of the cosh family is selected; that requires the calibration step. The declaration does not claim that the continuum is unnecessary for the full cost theorem, only for this algebraic identity.

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