dAlembert_diff_square
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume continuity or differentiability of H.
- Does not derive the d'Alembert equation from the Recognition Composition Law.
- Applies only when the relation holds for every real t and u.
- Derives solely the squared difference, not higher-order or differential consequences.
formal statement (Lean)
139lemma dAlembert_diff_square
140 (H : ℝ → ℝ)
141 (h_one : H 0 = 1)
142 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
143 ∀ t u,
144 (H (t+u) - H (t-u))^2 = 4 * ((H t)^2 - 1) * ((H u)^2 - 1) := by
proof body
Tactic-mode proof.
145 intro t u
146 have h_sum : H (t+u) + H (t-u) = 2 * H t * H u := h_dAlembert t u
147 have h_prod : H (t+u) * H (t-u) = (H t)^2 + (H u)^2 - 1 :=
148 dAlembert_product H h_one h_dAlembert t u
149 calc
150 (H (t+u) - H (t-u))^2
151 = (H (t+u) + H (t-u))^2 - 4 * (H (t+u) * H (t-u)) := by ring
152 _ = (2 * H t * H u)^2 - 4 * ((H t)^2 + (H u)^2 - 1) := by
153 simp [h_sum, h_prod]
154 _ = 4 * ((H t)^2 - 1) * ((H u)^2 - 1) := by ring
155