cosh_satisfies_dalembert
The hyperbolic cosine satisfies the d'Alembert functional equation H(t+u) + H(t-u) = 2 H(t) H(u) for all real t and u. Number theorists examining multiplicative ledger structures in Recognition Science cite this to confirm that the shifted J-cost obeys the same addition law as wave-equation solutions. The verification expands the hyperbolic addition and subtraction identities and reduces the identity by algebraic cancellation.
claim$H(t+u) + H(t-u) = 2 H(t) H(u)$ holds for all real $t,u$ when $H = $ hyperbolic cosine.
background
The module treats natural numbers as transactions on a discrete multiplicative ledger, with primes as the irreducible entries whose unique factorization supplies the balance sheet. The d'Alembert equation is introduced to force zeros of solutions onto vertical lines, supplying one of the three pillars (theorem, model, hypothesis) toward a Recognition-Science account of the Riemann Hypothesis. Upstream, the shifted cost is defined by H(x) = J(x) + 1 = ½(x + x⁻¹); under this reparametrization the Recognition Composition Law becomes exactly the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The log-coordinate lift G_F(t) = F(e^t) and its further shift H_F(t) = G_F(t) + 1 are the standard bridges between the multiplicative J-cost and the additive d'Alembert form.
proof idea
The term proof opens with intro t u, rewrites the left-hand side via the library lemmas Real.cosh_add and Real.cosh_sub, then closes with the ring tactic that cancels the resulting trigonometric polynomials.
why it matters in Recognition Science
The declaration supplies the concrete verification that the RS-native cost function (shifted J) satisfies d'Alembert, thereby grounding the module's claim that d'Alembert zero structure is a theorem rather than a hypothesis. It sits inside the larger program that identifies the J-cost symmetry with the completed zeta functional equation and predicts the Riemann Hypothesis from ledger conservation; the open gap remains whether the Euler product itself imposes d'Alembert-type constraints on the completed zeta.
scope and limits
- Does not prove uniqueness of solutions to the d'Alembert equation.
- Does not derive any link between the cost function and the zeta function.
- Does not address the gravitational constant or other RS-native constants.
- Does not treat the case of complex arguments or analytic continuation.
formal statement (Lean)
60theorem cosh_satisfies_dalembert : SatisfiesDAlembert Real.cosh := by
proof body
Term-mode proof.
61 intro t u
62 rw [Real.cosh_add, Real.cosh_sub]
63 ring
64
65/-- The RS cost function G(t) = J(e^t) = cosh(t) - 1 shifted by 1
66 gives H(t) = cosh(t) which satisfies d'Alembert. -/