F_forced_to_Jcost
plain-language theorem explainer
Under normalization, symmetry, C^2 smoothness, calibration of the second derivative at zero, consistency with a combiner P, and interaction, any cost function F must equal the J-cost J(x) = (x + x^{-1})/2 - 1 for x > 0. Researchers deriving physics from the single Recognition functional equation cite this to fix the cost function uniquely before deriving the RCL. The argument lifts to the log-coordinate G, uses interaction to force a hyperbolic ODE, solves it uniquely via initial conditions as cosh(t) - 1, and substitutes back.
Claim. Let $F : (0,∞) → ℝ$ and $P : ℝ → ℝ → ℝ$. Suppose $F(1) = 0$, $F(x) = F(x^{-1})$ for all $x > 0$, $F$ is twice continuously differentiable, the second derivative of the log-lift $G(t) = F(e^t)$ at $t=0$ equals 1, $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x,y > 0$, and $F$ admits interaction. Then $F(x) = (x + x^{-1})/2 - 1$ for all $x > 0$.
background
The AnalyticBridge module establishes that structural axioms plus interaction force the d'Alembert functional equation on the cost function. The log-lift is defined by $G(t) := F(e^t)$, converting the multiplicative consistency relation into an additive form on the real line. Upstream results include the dalembert_identity theorem, which states that Jcost satisfies J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), and the Cost.FunctionalEquation reparametrization that identifies G with the shifted lift H(t) = G(t) + 1.
proof idea
The proof first invokes interaction_implies_entangling to obtain that P is entangling. It then applies entangling_combiner_forces_hyperbolic to deduce that G satisfies the hyperbolic ODE. Initial conditions G(0) = 0 and G'(0) = 0 are recovered from G_zero and even_function_deriv_zero. hyperbolic_ode_unique then yields the unique solution G(t) = cosh(t) - 1. Back-substitution t = log x followed by the identity cosh(log x) = (x + x^{-1})/2 produces F(x) = Jcost(x).
why it matters
This theorem is invoked by full_inevitability to conclude that both F and P are uniquely forced, and by P_forced_to_RCL to identify P with the RCL combiner. It supplies the J-uniqueness step (T5) in the UnifiedForcingChain, showing that interaction eliminates any additive alternative and forces the hyperbolic form required for the eight-tick octave and D = 3. The result closes the analytic gap between the consistency equation and the Recognition functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.