full_inevitability
plain-language theorem explainer
Under the structural axioms of normalization, symmetry, twice-differentiable smoothness, second-derivative calibration of the log-lift, and the interaction gate, any cost function F and combiner P are forced to the J-cost and the Recognition Composition Law. Researchers tracing the derivation of d'Alembert structure from recognition axioms cite this as the capstone of the analytic bridge. The proof is a direct conjunction of the two prior inevitability theorems, one for F and one for P.
Claim. Let $F: (0,∞) → ℝ$ satisfy $F(1)=0$, $F(x)=F(x^{-1})$ for all $x>0$, be twice continuously differentiable, and have the second derivative of its log-lift $G(t)=F(e^t)$ equal to 1 at $t=0$. Let $P: ℝ×ℝ → ℝ$ satisfy the consistency relation $F(xy)+F(x/y)=P(F(x),F(y))$ for all $x,y>0$, and assume $F$ satisfies the interaction gate (the combiner is non-additive for some pair). Then $F(x)=(x+x^{-1})/2-1$ for all $x>0$, and $P(u,v)=2uv+2u+2v$ for all $u,v≥0$.
background
The module proves the analytic bridge: structural axioms plus interaction force the log-lift of F to satisfy d'Alembert's functional equation. G_of is the log-lift defined by G(t) := F(exp t). HasInteraction asserts existence of x,y>0 such that F(xy)+F(x/y) ≠ 2F(x)+2F(y), i.e., the combiner P is non-additive. Upstream, F_forced_to_Jcost states that the axioms plus interaction force F to equal Jcost. P_forced_to_RCL states that once F equals Jcost the consistency equation forces P to the Recognition Composition Law form on the non-negative quadrant.
proof idea
The term proof uses constructor to split the target conjunction, then applies F_forced_to_Jcost to obtain the first conjunct and P_forced_to_RCL to obtain the second. Each of those lemmas proceeds by showing interaction implies an entangling combiner, which forces a hyperbolic ODE on the log-lift, which with the given boundary conditions yields uniqueness.
why it matters
This is the main theorem of the analytic bridge. It closes the chain from the interaction gate through the necessity gates to the unique J-cost and RCL combiner. In the Recognition framework it realizes T5 J-uniqueness together with the Recognition Composition Law under the interaction hypothesis, confirming that interaction is the fundamental gate forcing d'Alembert structure with no third option between additive and hyperbolic cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.