dAlembert_diff_sq
plain-language theorem explainer
Any real function H obeying the additive d'Alembert identity H(s+t)+H(s−t)=2 H(s)H(t) with H(0)=1 satisfies (H(s+t)−H(s−t))² = 4(H(s)²−1)(H(t)²−1). Analysts and RS foundation work cite this as the completeness-free sinh-square identity for the shifted cost. The proof is pure algebra: expand the square, substitute the sum law, product identity, and duplication formula, then ring-normalize.
Claim. Let $H:\mathbb{R}\to\mathbb{R}$ satisfy $H(s+t)+H(s-t)=2H(s)H(t)$ for all real $s,t$, and $H(0)=1$. Then for all $s,t$, $\bigl(H(s+t)-H(s-t)\bigr)^2=4\bigl(H(s)^2-1\bigr)\bigl(H(t)^2-1\bigr)$.
background
In Recognition Science the native cost is $J(x)=\frac12(x+x^{-1})-1$. The shifted cost $H:=J+1$ converts the Recognition Composition Law into the classical d'Alembert (cosine/cosh) functional equation $H(xy)+H(x/y)=2H(x)H(y)$. The present module works in the additive reparametrization of that equation: $H(s+t)+H(s-t)=2H(s)H(t)$, with normalization $H(0)=1$.
Sibling lemmas already record the product identity $H(s+t)H(s-t)=H(s)^2+H(t)^2-1$ (after duplication) and the duplication formula $H(2u)=2H(u)^2-1$. Those two facts, together with the sum law itself, are the only inputs. No continuity, measurability, or completeness hypothesis appears; the identity is field-algebraic over $\mathbb{R}$.
The square identity is the magnitude half of the §9 sign crux: it is the discrete analogue of $\sinh^2 a,\sinh^2 b$ for the cosh family, leaving only the choice of square-root sign for the monotone case.
proof idea
Fix arbitrary $s,t$. Instantiate the d'Alembert sum law at $(s,t)$, the product identity dAlembert_prod at $(s,t)$, and the duplication formula dAlembert_duplication at both $s$ and $t$. Rewrite the product identity by substituting the two duplication equalities so that the right-hand side becomes an expression in $H(s)^2-1$ and $H(t)^2-1$.
Algebraically expand $(H(s+t)-H(s-t))^2$ as $(H(s+t)+H(s-t))^2-4H(s+t)H(s-t)$. Replace the sum by the d'Alembert right-hand side and the product by the rewritten product identity, then finish by ring. The whole argument is equational; no case splits or analytic limits.
why it matters
This lemma is the magnitude half of the §9 sign crux in the Primitive Recognition Calculus. Its immediate parent dAlembert_diff_eq_of_monotone takes the nonnegative square root under monotonicity on $[0,\infty)$, recovering the cosh addition formula $H(s+t)-H(s-t)=2\sqrt{H(s)^2-1},\sqrt{H(t)^2-1}$ with order alone fixing the sign that classical proofs extract from continuity. That resolution feeds the uniqueness cascade for monotone d'Alembert solutions (the cosh family), which is the analytic backbone of T5 J-uniqueness: $J(x)=\cosh(\log x)-1$.
Downstream, costLambda_successor_increment_tendsto sits in the native-cost uniqueness module and uses the same algebraic skeleton when calibrating the $\delta$-act ladder against the scale family. Completeness-free magnitude control is what lets the forcing chain separate order structure from topological hypotheses: monotonicity pins the sign; algebra pins the square. The open residual after this lemma is only the global classification under monotonicity, not the local difference identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.