analytic_bridge_full
plain-language theorem explainer
The full analytic bridge theorem shows that a cost function F obeying normalization at unity, inversion symmetry, C^2 smoothness, interaction, and multiplicative consistency with a combiner P that extends the recognition composition law forces the shifted log-lift H to satisfy the d'Alembert equation. Researchers closing the consistency-to-dynamics step in Recognition Science would cite this result. The proof is a one-line wrapper that invokes the base analytic_bridge theorem after fixing P to its explicit RCL expression via the added extension
Claim. Let $F:ℝ→ℝ$ satisfy $F(1)=0$, $F(x)=F(x^{-1})$ for $x>0$, and be twice continuously differentiable. Let $P:ℝ→ℝ→ℝ$ be twice differentiable such that $F(xy)+F(x/y)=P(F(x),F(y))$ for positive $x,y$, $F$ has interaction, and $P(u,v)=2uv+2u+2v$ for all real $u,v$. Then the shifted log-lift $H(t):=F(e^t)+1$ satisfies $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$.
background
The module proves that structural axioms on a cost function force the d'Alembert equation on its log-lift. The log-lift is defined by G_of F t := F(exp t) and the shifted version by H_of F t := G_of F t + 1. The base analytic_bridge theorem assumes the combiner P takes the explicit RCL form P u v = 2 u v + 2 u + 2 v and concludes the d'Alembert equation for H. This full version adds the hypothesis that P extends to that form on all of ℝ², deriving it from interaction as per the module strategy of differentiating the consistency equation and using boundary conditions to constrain Q.
proof idea
The proof is a one-line wrapper that applies the analytic_bridge theorem to the given F, P, and hypotheses, substituting the explicit RCL form supplied by hPext for the required hPrcl hypothesis.
why it matters
This theorem completes the analytic bridge in the DAlembert module by showing how interaction forces the combiner to the RCL form, which in turn yields the d'Alembert equation for the log-lift. It supports the broader Recognition Science program of deriving wave equations from the recognition composition law and the J-uniqueness step. No direct downstream uses are listed, but it underpins the inevitability of hyperbolic structures with no third option between additive and d'Alembert cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.