dAlembert_S_add_of_monotone
plain-language theorem explainer
Under the d'Alembert identity H(s+t)+H(s-t)=2Hs Ht with H(0)=1 and H monotone on [0,∞), the companion S(x)=√(H(x)²−1) obeys the sinh addition law S(s+t)=Hs·St+Ss·Ht whenever 0≤t≤s. Cited by anyone deriving the cosh family from a monotone cost without completeness. Proof squares the H-addition formula and extracts the nonnegative root.
Claim. Let $H:\mathbb{R}\to\mathbb{R}$ satisfy $H(s+t)+H(s-t)=2H(s)H(t)$ for all real $s,t$, with $H(0)=1$, and suppose $H$ is monotone on $[0,\infty)$. Then for all $s,t$ with $0\le t\le s$, $$\sqrt{H(s+t)^2-1}=H(s)\sqrt{H(t)^2-1}+\sqrt{H(s)^2-1}\,H(t).$$
background
In Recognition Science the shifted cost $H=J+1$ converts the Recognition Composition Law into the classical d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$. In additive coordinates the same identity reads $H(s+t)+H(s-t)=2H(s)H(t)$. The normalization $H(0)=1$ is forced by $J(1)=0$.
The companion function $S(x)=\sqrt{H(x)^2-1}$ is the formal sinh partner of $H$. On the half-line where $H$ is monotone and $H\ge 1$, both square roots are well-defined and nonnegative. The module develops the monotone route to uniqueness of the cost form: d'Alembert plus monotonicity on $[0,\infty)$ forces $H=\cosh(c,\cdot)$ without invoking completeness of $\mathbb{R}$.
Upstream, $H\ge 1$ on $[0,\infty)$ is already available (dAlembert_ge_one_of_monotone), and the ordinary $H$-addition formula $H(s+t)=Hs Ht+Ss St$ is proved as dAlembert_add_of_monotone. The present lemma is the matching $S$-addition identity.
proof idea
Fix $0\le t\le s$. Monotonicity plus $H(0)=1$ gives $H s\ge 1$ and $H t\ge 1$, so both $H^2-1$ terms are nonnegative and the candidate right-hand side is a sum of nonnegative products.
Invoke the already-proved $H$-addition identity dAlembert_add_of_monotone. Square the proposed right-hand side; after substituting $H(s+t)=Hs Ht+Ss St$ and cancelling via $(\sqrt{u})^2=u$, the square equals $H(s+t)^2-1$. Taking the nonnegative square root recovers the claim (Real.sqrt_sq).
why it matters
This is the second half of the addition package needed for the multiplicative lift $\varphi(x)=H(x)+S(x)$. Downstream, phi_mul_of_monotone multiplies the $H$- and $S$-addition formulae to obtain $\varphi(s+t)=\varphi(s)\varphi(t)$ on $0\le t\le s$. Because $\varphi>0$, $\log\circ\varphi$ is additive and monotone on $[0,\infty)$, hence linear by monotone_additive_isLinear; the linear exponent yields $H=\cosh(c,\cdot)$.
That completeness-free derivation of the cosh family is the monotone route to T5-style $J$-uniqueness inside the Primitive Recognition Calculus. The same identity is consumed later by the $\delta$-act ladder analysis (costLambda_successor_increment_tendsto), which reads the calibration invariant $c^2$ off discrete successor increments. Framework landmark: forces the hyperbolic cost form that underlies the RCL and the $\phi$-ladder mass formula, without analytic completeness hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.