H_dAlembert_of_composition
plain-language theorem explainer
Derives the additive d'Alembert equation for the shifted cost from the multiplicative composition law on F. Researchers tracing the T5 J-uniqueness step in the Recognition Science forcing chain cite it to bridge Aczel regularity to the kernel without JensenSketch. The proof converts the composition law to DirectCoshAdd on G F via an equivalence lemma, then applies ring tactics in a calc block to match the target identity.
Claim. If a function $F : ℝ → ℝ$ satisfies the composition law, let $H_F$ denote its shifted cost function. Then $H_F(t + u) + H_F(t - u) = 2 H_F(t) H_F(u)$ for all real $t, u$.
background
The AczelClassification module packages the d'Alembert forcing chain supplied by the Aczel classification theorem: continuous d'Alembert solutions are smooth, and smoothness yields the calibrated ODE kernel satisfying H'' = H. The shifted cost is defined by H(x) = J(x) + 1 = ½(x + x^{-1}). Under this shift the Recognition Composition Law becomes the multiplicative d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
The proof defines Gf := G F and obtains DirectCoshAdd Gf by applying CoshAddIdentity_implies_DirectCoshAdd to the forward direction of composition_law_equiv_coshAdd F on hComp. It introduces t and u, retrieves the cosh-add identity, and uses a calc block: ring to add the constants, simpa to substitute the identity, then ring again to reach 2 (Gf t + 1)(Gf u + 1). A final simpa recovers the H form.
why it matters
This supplies the additive d'Alembert equation required by the downstream theorem primitive_to_uniqueness_of_kernel, the official public T5 result that uses AczelRegularityKernel as the sole regularity bridge to establish cost-kernel uniqueness. It advances the T5 J-uniqueness step in the forcing chain (T0-T8) and the RCL, closing the d'Alembert seam explicitly without routing through JensenSketch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.