separable_combiner_forces_flat
plain-language theorem explainer
Under normalization F(1)=0, symmetry F(x)=F(1/x) for x>0, twice continuous differentiability of F, and calibration of the second derivative of its log-lift at zero, if the combiner P is separable and satisfies the boundary conditions P(u,0)=2u and P(0,v)=2v, then the log-lift G(t)=F(e^t) satisfies the flat ODE G''=1. Analysts working on the consistency-to-ODE bridge in Recognition Science would cite this result to separate the additive and interacting cases. The proof reduces separability to an additive form for P, substitutes to obtain theflat
Claim. Let $F:ℝ→ℝ$ and $P:ℝ→ℝ→ℝ$ satisfy $F(1)=0$, $F(x)=F(x^{-1})$ for all $x>0$, $F$ twice continuously differentiable, the second derivative of $G(t)=F(e^t)$ at $t=0$ equals 1, $F(xy)+F(x/y)=P(F(x),F(y))$ for $x,y>0$, $P$ separable, and $P(u,0)=2u$, $P(0,v)=2v$ for all $u,v$. Then $G$ satisfies the flat ODE $G''=1$.
background
In the AnalyticBridge module the log-lift is defined by $G(t)=F(e^t)$. The module establishes the bridge from structural axioms on cost functions to d'Alembert equations by differentiating consistency relations and constraining the combiner $P$. The theorem relies on upstream results including G_zero which shows $G(0)=0$ from $F(1)=0$, log_consistency which relates the consistency equation to the combiner, and separable_forces_additive which forces separable $P$ to be additive $P(u,v)=2u+2v$. From the module doc: '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 proof intros the hypotheses, applies separable_forces_additive to obtain that $P(u,v)=2u+2v$, substitutes this into the consistency equation via log_consistency to derive the flat functional equation $G(t+u)+G(t-u)=2G(t)+2G(u)$, and then invokes separable_forces_flat_ode with the zero, derivative, calibration, and smoothness conditions to conclude that $G$ satisfies the flat ODE.
why it matters
This result establishes the separable case in the differentiation_key_lemma, which connects combiner type to ODE type. It fills the additive branch of the bridge theorem in the AnalyticBridge module, showing that separable combiners force the flat ODE $G''=1$. In the Recognition Science framework this separates the non-interacting case from the entangling case that forces the hyperbolic ODE $G''=G+1$, consistent with the RCL and the forcing chain toward d'Alembert structure. It touches the open question of full formalization of the classical ODE results noted in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.