dAlembert_diff_square
plain-language theorem explainer
This lemma derives a squared difference identity for functions satisfying the d'Alembert equation with H(0) equal to 1. Researchers proving analytic properties of the J-cost in the T5 uniqueness chain would cite it when moving from the functional equation to continuity or curvature results. The proof is a short algebraic reduction that invokes a companion product identity and simplifies via ring expansion.
Claim. Let $H : ℝ → ℝ$ satisfy $H(0) = 1$ and $H(t+u) + H(t-u) = 2 H(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)$.
background
In Recognition Science the J-cost obeys the Recognition Composition Law. The reparametrization H(x) = J(x) + 1 converts this into the additive d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u), with the normalization H(0) = 1. The module supplies supporting lemmas for the T5 J-uniqueness argument. The present lemma depends on the product identity that states H(t+u) H(t-u) = (H t)^2 + (H u)^2 - 1 under the same hypotheses.
proof idea
The proof recalls the sum relation directly from the hypothesis. It applies the dAlembert_product lemma to obtain the matching product relation. It then substitutes both into the algebraic identity (a - b)^2 = (a + b)^2 - 4ab and reduces the resulting polynomial expression with ring tactics.
why it matters
The identity supplies an algebraic stepping stone inside the T5 cost-uniqueness proof. It is invoked by the downstream theorem that extracts continuity of H from a log-curvature hypothesis. In the larger framework it helps convert the Recognition Composition Law into concrete analytic consequences that feed the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.