dAlembert_with_unit_calibration
plain-language theorem explainer
Under the d'Alembert functional equation with unit second-derivative calibration at the origin, any C² function H must coincide with the hyperbolic cosine. Physicists deriving the Recognition Science cost function from the forcing chain cite this to fix the canonical form of H. The argument first differentiates the functional equation to produce the ODE H'' = H''(0) H, substitutes the calibration H''(0)=1, and invokes ODE uniqueness.
Claim. Let $H : ℝ → ℝ$ be twice continuously differentiable and satisfy $H(0)=1$ together with $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$. If additionally $H'(0)=0$ and $H''(0)=1$, then $H(t)=cosh t$ for all $t$.
background
The Fourth Gate module formalizes the d'Alembert structure condition on the shifted cost function. SatisfiesDAlembert H holds when H(0)=1 and the functional equation H(t+u)+H(t-u)=2 H(t) H(u) is true for all t,u; this is the classical d'Alembert equation whose continuous solutions are hyperbolic cosines. In the Recognition Science setting, H arises as the log-lift of the J-cost via H(t)=J(e^t)+1, so that the Recognition Composition Law reduces exactly to this equation. The module records that in the Option A formulation this structure is derived from the curvature gate rather than imposed independently.
proof idea
The proof invokes dalembert_deriv_ode on H, hSmooth and the functional part of hDA to obtain ∀x, deriv(deriv H) x = deriv(deriv H) 0 · H x. It substitutes the calibration hCalib to replace the constant factor by 1, yielding the ODE H''=H. From hDA it extracts H(0)=1; together with the given hDeriv0 it applies ode_cosh_uniqueness_contdiff to conclude H=cosh everywhere.
why it matters
This result supplies the calibrated form of H required by dAlembert_forces_Gcosh, which forces G=cosh-1. It completes the cross-check between the functional-equation viewpoint and the curvature gate inside the Fourth Gate module. Within the forcing chain it confirms the J-uniqueness step (T5) by exhibiting the explicit cosh solution that matches the self-similar fixed point phi, with the eight-tick octave and D=3 emerging downstream from the same calibrated structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.