separable_forces_flat_ode
plain-language theorem explainer
The separable forces flat ODE theorem shows that any twice continuously differentiable real function G obeying the additive consistency relation G(t+u) + G(t-u) = 2G(t) + 2G(u) for all t,u, together with the boundary data G(0)=0, G'(0)=0 and G''(0)=1, must satisfy the constant-curvature ODE G''(t)=1 everywhere. Researchers deriving the flat branch of the Recognition Science analytic bridge between separable interactions and d'Alembert structure would cite this result. The proof works by twice differentiating the functional equation with respect
Claim. Let $G : {R} {to} {R}$ be twice continuously differentiable and satisfy $G(t+u) + G(t-u) = 2G(t) + 2G(u)$ for all real $t,u$, with $G(0)=0$, $G'(0)=0$ and $G''(0)=1$. Then $G''(t)=1$ for all real $t$.
background
The AnalyticBridge module establishes the bridge theorem: structural axioms plus interaction force the log-lift $H(t) = F(e^t) + 1$ to obey the d'Alembert functional equation. The present result treats the separable (non-interacting) case of the underlying consistency equation, where the combiner reduces to the additive form $P = 2u + 2v$ after boundary conditions. This contrasts with the entangling case handled by the sibling hyperbolic ODE theorem. Upstream results supply the required smoothness infrastructure (ContDiff) and the definition of the log-consistency equation itself.
proof idea
The tactic proof begins by fixing an arbitrary $t$ and introducing auxiliary maps $f(u) = G(t+u) + G(t-u)$ and $g(u) = 2G(t) + 2G(u)$. It first shows $f = g$ by extensionality from the given functional equation. Differentiability of $G$ (from ContDiff 2) is used to compute the first derivative of $f$, then the second derivative at $u=0$, yielding $2G''(t)$. The second derivative of $g$ at zero is shown to equal 2 by the calibration $G''(0)=1$. Equating the two second derivatives and applying linarith produces $G''(t)=1$.
why it matters
This theorem supplies the separable branch of the Analytic Bridge, feeding directly into the downstream result separable_combiner_forces_flat that concludes $G''=1$ for any separable combiner. It completes the dichotomy: separable interactions produce flat geometry while entangling interactions produce the hyperbolic ODE $G''=G+1$. The result therefore sharpens the claim that interaction is required to generate non-flat structure, consistent with the module's strategy of differentiating consistency equations and using boundary data to constrain the combiner.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.