entangling_combiner_forces_hyperbolic
plain-language theorem explainer
The theorem shows that an entangling combiner P of explicit RCL form forces the log-lift G of a normalized symmetric smooth cost function F to satisfy the hyperbolic ODE G'' = G + 1. Researchers deriving the Recognition Science bridge from interaction axioms to d'Alembert structure cite this as the key step linking combiner type to ODE type. The proof first converts the multiplicative consistency equation to the additive RCL form on G via log-consistency, then applies the specialized entangling ODE theorem with the supplied boundary conditions.
Claim. Let $G(t) := F(e^t)$. Suppose $F(1) = 0$, $F(x) = F(x^{-1})$ for all $x > 0$, $F$ is twice continuously differentiable, $G''(0) = 1$, the consistency relation $F(xy) + F(x/y) = P(F(x), F(y))$ holds for $x, y > 0$, $P$ is entangling, and $P(u, v) = 2uv + 2u + 2v$. Then $G''(t) = G(t) + 1$ for all real $t$.
background
In the Analytic Bridge module the log-lift is defined by $G(t) := F(e^t)$. The multiplicative consistency hypothesis on $F$ translates, by the upstream log_consistency theorem, into the additive equation $G(t+u) + G(t-u) = P(G(t), G(u))$. The module shows that interaction forces the combiner $P$ into the specific RCL form $P(u,v) = 2uv + 2u + 2v$, which is the d'Alembert structure. SatisfiesHyperbolicODE is the definition asserting that $G''(t) = G(t) + 1$ everywhere. The upstream entangling_forces_hyperbolic_ode theorem assumes precisely this RCL form together with the initial conditions $G(0) = 0$, $G'(0) = 0$, $G''(0) = 1$ and concludes the ODE. G_zero derives $G(0) = 0$ directly from $F(1) = 0$. The local theoretical setting is the proof that consistency plus interaction admits no third option between additive and d'Alembert cases.
proof idea
The proof first constructs the functional equation hFE for $G$ by applying log_consistency to the given consistency hypothesis on $F$ and rewriting the result with the explicit RCL hypothesis. It then invokes the upstream theorem entangling_forces_hyperbolic_ode on $G_of F$, supplying hFE, the zero condition from G_zero, the first-derivative zero obtained from symmetry and normalization, the calibration $G''(0) = 1$, and the smoothness of $G$ inherited from $F$.
why it matters
This result is invoked by differentiation_key_lemma to connect combiner type to ODE type and feeds directly into F_forced_to_Jcost, which concludes that $F$ must be the J-cost function. It fills the entangling case of the bridge theorem stated in the module doc-comment. In the Recognition Science framework the step belongs to the forcing chain that produces J-uniqueness (T5) and the subsequent phi-ladder, eight-tick octave, and $D = 3$ spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.