entangling_forces_hyperbolic_ode
plain-language theorem explainer
Any twice continuously differentiable function G satisfying the entangling functional equation G(t+u) + G(t-u) = 2G(t)G(u) + 2G(t) + 2G(u) for all real t and u, together with the boundary conditions G(0) = 0, G'(0) = 0 and G''(0) = 1, obeys the hyperbolic ODE G''(t) = G(t) + 1. Recognition Science derivations of wave equations from the Recognition Composition Law cite this bridge result for the entangling case. The proof shifts to the auxiliary function H = G + 1, recovers the standard d'Alembert equation, and applies the differentiation lemma.
Claim. Let $G : ℝ → ℝ$ be twice continuously differentiable and satisfy $G(t+u) + G(t-u) = 2G(t)G(u) + 2G(t) + 2G(u)$ for all real $t,u$, with $G(0)=0$, $G'(0)=0$, and $G''(0)=1$. Then $G''(t) = G(t) + 1$ for all $t$.
background
The Analytic Bridge module establishes that structural axioms plus interaction force the d'Alembert form. The Recognition Composition Law states J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y); the shift H(x) = J(x) + 1 converts it to the d'Alembert equation H(xy) + H(x/y) = 2H(x)H(y). The function G here is the log-reparametrization G_F(t) = F(exp t). The upstream lemma dalembert_deriv_ode asserts that any C² solution of the d'Alembert equation satisfies the second-order ODE H''(t) = H''(0) H(t).
proof idea
The proof introduces the auxiliary H := G + 1, verifies that H satisfies the d'Alembert equation H(x+y) + H(x-y) = 2H(x)H(y) by direct substitution into the given functional equation followed by linarith, confirms ContDiff ℝ 2 H, invokes dalembert_deriv_ode to obtain H''(t) = H''(0) H(t), computes H''(0) = 1 from the supplied G''(0) = 1 via the chain rule on the shift, and substitutes back to reach G''(t) = G(t) + 1.
why it matters
This theorem supplies the ODE for the entangling case inside the analytic bridge and feeds directly into the parent result entangling_combiner_forces_hyperbolic, which asserts that an entangling combiner forces G'' = G + 1 on the log-lift of F. It closes the step from the RCL form to the hyperbolic wave equation, aligning with the J-uniqueness fixed point and the eight-tick octave in the forcing chain. The module doc-comment notes that these ODE results are axiomatized classical calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.