dAlembert_diff_square
plain-language theorem explainer
Algebraic identity for d'Alembert solutions: the squared difference equals four times the product of (H squared minus one) terms. Uniqueness proofs for the hyperbolic cosine solution in Recognition Science T5 would cite this result. The derivation combines the sum hypothesis with the product lemma via direct expansion and ring simplification.
Claim. Let $H:ℝ→ℝ$ satisfy $H(0)=1$ and $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$. Then $(H(t+u)-H(t-u))^2=4((H(t))^2-1)((H(u))^2-1)$ for all real $t,u$.
background
In the Cost.FunctionalEquation module, which supplies helpers for the T5 cost uniqueness proof, H is the reparametrization H_F(t)=G_F(t)+1. Upstream, Algebra.CostAlgebra.H defines the shifted cost H(x)=J(x)+1=½(x+x⁻¹), converting the Recognition Composition Law into the d'Alembert equation H(xy)+H(x/y)=2H(x)H(y). The module states it provides lemmas for the T5 cost uniqueness proof. This lemma relies on the sibling dAlembert_product, which derives the product identity H(t+u)H(t-u)=(Ht)²+(Hu)²-1 under the same hypotheses.
proof idea
The proof introduces the sum relation from the d'Alembert hypothesis. It applies the dAlembert_product lemma to obtain the product identity. A calc block then rewrites the target square as (sum)² minus four times the product, substitutes the two relations, and reduces via ring tactics.
why it matters
This lemma supports dAlembert_continuous_of_log_curvature, which derives continuity from log curvature. It advances the T5 J-uniqueness step in the forcing chain, where J(x)=(x+x⁻¹)/2-1 is forced as the unique solution. The result helps establish properties needed for the phi fixed point and eight-tick octave in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.