dAlembert_forces_Jcost
plain-language theorem explainer
Any twice continuously differentiable cost function F on positive reals that vanishes at unity, obeys reciprocal symmetry, meets the second-derivative calibration after log-lift, and satisfies the d'Alembert condition on its shifted log-lift must equal the J-cost J(x) = cosh(log x) - 1. Workers on the Recognition Science inevitability chain cite this to close the fourth gate. The argument lifts F to an even smooth G, invokes the companion result forcing G(t) = cosh(t) - 1, and substitutes back via the hyperbolic identity.
Claim. Let $F : ℝ → ℝ$ satisfy $F(1) = 0$, $F(x) = F(x^{-1})$ for $x > 0$, be twice continuously differentiable, have the second derivative of the log-lifted map equal to 1 at zero, and let the shifted log-lift $H(t) = F(e^t) + 1$ satisfy the d'Alembert equation $H(t+s) + H(t-s) = 2H(t)H(s)$. Then $F(x) = (x + x^{-1})/2 - 1$ for all $x > 0$.
background
The Fourth Gate module formalizes the d'Alembert structure condition as the final constraint. HasDAlembert F holds precisely when the shifted log-lift H(t) = F(exp t) + 1 obeys the classical d'Alembert functional equation. This sits after the curvature gate and rests on the companion theorem dAlembert_forces_Gcosh, which states that d'Alembert structure plus calibration forces the log-lifted G to equal cosh minus one. The local setting follows the Option A formulation in which Gate 3 already yields the hyperbolic solution, rendering Gate 4 a derived cross-check via Aczél's classification of continuous solutions.
proof idea
The proof defines the log-lift G(t) = F(exp t) and verifies that G inherits smoothness, evenness, normalization at zero, and the calibration from the hypotheses on F. It then applies the upstream theorem dAlembert_forces_Gcosh to conclude G(t) = cosh(t) - 1. Substituting back via F(x) = G(log x) and the identity cosh(log x) = (x + x^{-1})/2 yields the J-cost expression.
why it matters
This theorem closes the fourth gate and feeds directly into full_inevitability_four_gates, which establishes that the structural axioms plus d'Alembert force F to equal J-cost and thereby the recognition composition law. It completes the T5 uniqueness step in the forcing chain T0-T8, confirming that the only cost function compatible with the axioms is the one derived from the phi fixed point. No open scaffolds remain in the inevitability equivalence after this result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.