analytic_bridge
plain-language theorem explainer
A function F obeying normalization at unity, inversion symmetry on positives, and multiplicative consistency with the RCL combiner P(u,v)=2uv+2u+2v forces its shifted log-lift H to obey the d'Alembert equation H(t+u)+H(t-u)=2H(t)H(u). Researchers deriving wave equations from consistency conditions in Recognition Science cite this bridge result. The proof is a direct algebraic reduction that applies the log-consistency lemma, substitutes the explicit form of P, and closes by linear arithmetic.
Claim. Let $F:ℝ→ℝ$ satisfy $F(1)=0$, $F(x)=F(x^{-1})$ for $x>0$, and $F(xy)+F(x/y)=P(F(x),F(y))$ for $x,y>0$ where $P(u,v)=2uv+2u+2v$. Let $G(t)=F(e^t)$ be the log-lift and $H(t)=G(t)+1$ the shifted version. Then $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$.
background
The module defines the log-lift $G_of F t = F(exp t)$ and the shifted version $H_of F t = G_of F t + 1$. The upstream result log_consistency converts multiplicative consistency of F into additive consistency for the log-lift: $G(t+u)+G(t-u)=P(G(t),G(u))$. The local setting is the Analytic Bridge module, whose goal is to show that structural axioms plus interaction force d'Alembert structure for the log-lift, with the explicit note that the RCL combiner turns log-consistency directly into the target equation.
proof idea
The proof introduces t and u, unfolds the definition of H_of, invokes log_consistency to obtain the additive relation for G_of, substitutes the assumed RCL form of P, rewrites, and closes the resulting identity with linarith.
why it matters
This supplies the core implication used by the full analytic_bridge_full theorem, which adds smoothness and calibration to derive the RCL form itself from interaction. The doc-comment states that multiplicative consistency plus the RCL combiner yields d'Alembert for the log-lift. The step supports the Recognition Science program of forcing d'Alembert structure from the Recognition Composition Law as part of the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.