Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcmonotone Dalembert D Alembert Diff

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Prcmonotone Dalembert D Alembert Diff

A single inequality, not calculus, decides which of two mirror-image curves a functional equation picks.

Verify this page

The sign fixed by order

The classical d'Alembert equation, H(s+t) + H(s−t) = 2H(s)H(t), governs functions whose value at a sum depends symmetrically on the two inputs. Its smooth solutions split into two families: the hyperbolic cosine, cosh(ct), which grows without bound, and the ordinary cosine, cos(ct), which oscillates. Both satisfy the same equation, so the equation alone cannot tell them apart. A standard way to separate them is to assume continuity or differentiability, analytic conditions that rule out the oscillating branch. The declaration dAlembert_diff_eq_of_monotone replaces that analytic assumption with a purely order-theoretic one.

The statement concerns a solution H of the d'Alembert equation with H(0) = 1 that is monotone, meaning nondecreasing, on the nonnegative real line. For any 0 ≤ t ≤ s, the declaration proves the exact difference formula: H(s+t) − H(s−t) = 2√(H(s)²−1) · √(H(t)²−1). This is the hyperbolic addition identity for cosh, written with square roots in place of the hyperbolic sine. The content is the sign: monotonicity forces H(s+t) ≥ H(s−t), so the difference is the nonnegative square root, not its negative. The oscillating cosine branch, which dips below 1 and would flip the sign, is excluded by order alone, with no continuity, no smoothness, and no least-upper-bound axiom. The proof uses only field operations, square roots, and the order structure of the real numbers.

In Recognition Science, this result is one brick in a larger argument that the framework's cost function is forced by monotonicity instead of by analytic regularity. The framework models recognition events as entries in a discrete ledger, a record of events, and derives its cost function from five plain conditions. The classical theorem used continuity to select the cosh branch; this declaration shows that monotonicity, an order property available on any ordered field, does the same work. It is a step toward showing the cost form can be derived without presupposing the continuum, leaving only a single unit-of-scale posit. The declaration itself, however, only fixes the sign in the difference formula; it does not by itself establish the full cost form, which requires further steps assembled elsewhere in the library.

What the declaration does not claim is equally precise. It does not assert that every monotone solution of the d'Alembert equation is cosh; that stronger conclusion, dAlembert_cosh_of_monotone, is a separate theorem requiring an evenness assumption. It does not apply to the cosine branch, which is monotone on no interval containing the origin. And it does not, on its own, derive the Recognition Science cost function; that derivation consumes this result as a lemma within a longer chain. The declaration is a sharp, narrow tool: it resolves the sign ambiguity in one identity using order alone.

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
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
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 assert that every monotone d'Alembert solution is cosh; that requires an evenness assumption in a separate theorem. The declaration does not apply to the cosine branch, which is not monotone on any interval containing the origin. The declaration does not by itself derive the Recognition Science cost function; it is one lemma in a longer chain.

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