differentiation_key_lemma
plain-language theorem explainer
The differentiation key lemma shows that a cost function F obeying normalization, inversion symmetry, C^2 smoothness and second-derivative calibration at the origin, paired with a combiner P obeying the consistency relation and the two boundary conditions, yields flat ODE behavior for the log-lift G when P is separable and hyperbolic ODE behavior when P is entangling. Analysts constructing the Recognition Science bridge from consistency to d'Alembert structure cite this classification result. The proof is a direct case split that dispatches to
Claim. Let $F:ℝ→ℝ$ satisfy $F(1)=0$, $F(x)=F(x^{-1})$ for $x>0$, and be $C^2$. Let $P:ℝ×ℝ→ℝ$ be $C^2$ and obey $F(xy)+F(x/y)=P(F(x),F(y))$ for $x,y>0$ together with $P(u,0)=2u$ and $P(0,v)=2v$. Write $G(t)=F(e^t)$. Assume also $G''(0)=1$. Then $P$ separable implies $G''=1$ everywhere, while $P$ entangling implies $G''=G+1$ everywhere.
background
The AnalyticBridge module develops the link between consistency relations on cost functions and the d'Alembert equation by differentiation. The log-lift is defined by G_of F (t) := F(exp t). The combiner P encodes interaction via the consistency hypothesis F(xy)+F(x/y)=P(Fx,Fy). IsSeparable and IsEntangling classify the algebraic form of P. The module states: 'This proves that the mere existence of a combiner with interaction forces the d'Alembert structure - there is no third option between additive (no interaction) and d'Alembert (interaction).'
proof idea
The term proof constructs the conjunction by two intro applications. The separable branch applies separable_combiner_forces_flat directly. The entangling branch first calls entangling_with_boundary_is_RCL to recover the explicit RCL form P u v = 2uv + 2u + 2v, then applies entangling_combiner_forces_hyperbolic.
why it matters
The lemma occupies the central position in the Analytic Bridge, converting the algebraic type of the interaction combiner into the differential equation satisfied by the log-lift. It supports the overall Bridge Theorem that consistency plus interaction forces d'Alembert structure. The entangling case directly instantiates the Recognition Composition Law from the T5 J-uniqueness step of the forcing chain. No open scaffolding remains; the classification is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.