H_dAlembert_of_G_RCL
plain-language theorem explainer
If G satisfies the Recognition Composition Law in additive form with G(0) = 0, then the shifted H = G + 1 obeys the d'Alembert equation H(t + u) + H(t - u) = 2 H(t) H(u). Researchers deriving the full unconditional inevitability of the J-cost and pairing function cite this bridge step. The proof is a direct algebraic expansion that adds 2 and factors the right-hand side via ring identities.
Claim. Let $G : ℝ → ℝ$ satisfy $G(0) = 0$ and the Recognition Composition Law $G(t + u) + G(t - u) = 2 G(t) G(u) + 2 G(t) + 2 G(u)$ for all real $t, u$. Define $H(t) := G(t) + 1$. Then $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$.
background
In the Full Unconditional RCL Inevitability module, any F : ℝ₊ → ℝ obeying normalization F(1) = 0, symmetry F(x) = F(1/x), C² smoothness, calibration G''(0) = 1 with G(t) = F(exp t), and multiplicative consistency F(xy) + F(x/y) = P(F(x), F(y)) for some P must force both F = J and the explicit pairing. The upstream CostAlgebra.H defines the shifted cost as H(x) = J(x) + 1 = ½(x + x⁻¹), under which the RCL becomes the standard d'Alembert equation H(xy) + H(x/y) = 2·H(x)·H(y). The G in this lemma is the log-coordinate reparametrization G(t) = F(exp t) from FunctionalEquation.G.
proof idea
The proof is a direct calc block. It rewrites the target left-hand side as G(t + u) + G(t - u) + 2. It substitutes the given RCL identity, then applies ring tactics three times to obtain 2 (G t + 1)(G u + 1), which is exactly 2 H(t) H(u).
why it matters
This lemma is invoked by full_inevitability_explicit and full_unconditional_inevitability in the same module, which close the argument that both the J-cost and P are forced with no assumption on P. It supplies the passage from the Recognition Composition Law to the d'Alembert equation that precedes the ODE analysis forcing the cosh solution. In the broader framework it links the RCL to the eight-tick octave and D = 3 via the d'Alembert solutions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.