cosh_satisfies_dalembert
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.