Jcost_satisfies_dAlembert
plain-language theorem explainer
The log-lift G(t) = cosh(t) of the J-cost function satisfies the d'Alembert equation G(t+u) + G(t-u) = 2 G(t) G(u) + 2 G(t) + 2 G(u) for all real t and u. Researchers tracing the Recognition Science consistency bridge from interaction axioms to hyperbolic solutions cite this verification that the candidate meets the required functional form. The proof is a direct algebraic check that invokes the standard hyperbolic addition and subtraction identities.
Claim. For all real numbers $t,u$, let $G(t) = (e^t + e^{-t})/2 - 1$. Then $G(t+u) + G(t-u) = 2 G(t) G(u) + 2 G(t) + 2 G(u)$. Equivalently, after the shift $H(t) = G(t) + 1$, one has $H(t+u) + H(t-u) = 2 H(t) H(u)$.
background
In the AnalyticBridge module the log-lift of a cost function F is the reparametrization G(t) = F(exp t). The J-cost is the explicit form J(x) = (x + x^{-1})/2 - 1 whose log-lift is exactly cosh(t) - 1. The module's central Bridge Theorem states that any F obeying the structural axioms plus an interaction condition forces its log-lift to obey the d'Alembert equation. An upstream result (entangling_combiner_forces_hyperbolic) shows that an entangling combiner implies the second-order ODE G'' = G + 1 whose solutions are hyperbolic cosines.
proof idea
The proof is a one-line term-mode wrapper. After intro t u and a simp that cancels the -1 + 1 shifts, it invokes Real.cosh_add t u and Real.cosh_sub t u, then applies linarith to obtain the required identity from the sum of the two addition formulas.
why it matters
This verification supplies the converse half of the inevitability axiom for F: once the hyperbolic ODE is solved, the resulting G must satisfy the original d'Alembert relation demanded by the structural axioms. It therefore closes the chain Interaction implies Entangling implies Hyperbolic ODE implies G = cosh - 1 implies F = Jcost. In the larger framework it confirms that the T5 J-uniqueness fixed point is compatible with the Recognition Composition Law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.