analytic_bridge
The analytic bridge theorem shows that a cost function F with F(1)=0, inversion symmetry for positive arguments, and multiplicative consistency under the combiner P(u,v)=2uv+2u+2v lifts via the shifted log-lift H(t)=F(exp t)+1 to satisfy d'Alembert's equation H(t+u)+H(t-u)=2H(t)H(u). Researchers deriving wave structures from recognition costs or functional equations in the forcing chain would cite it. The proof is a direct algebraic reduction that invokes the log-consistency lemma, substitutes the explicit P form, and closes with linear-arith.
claimLet $F:ℝ→ℝ$ satisfy $F(1)=0$, $F(x)=F(x^{-1})$ for all $x>0$, and $F(xy)+F(x/y)=P(F(x),F(y))$ for all $x,y>0$, where $P(u,v)=2uv+2u+2v$. Define the shifted log-lift by $H(t):=F(e^t)+1$. Then $H(t+u)+H(t-u)=2H(t)H(u)$ holds for all real $t,u$.
background
The AnalyticBridge module establishes that structural axioms on a cost function plus a specific combiner force d'Alembert structure on its log-lift. The log-lift is G_of F t := F(exp t) and the shifted version is H_of F t := G_of F t +1. The upstream log_consistency result states that multiplicative consistency on F transfers to additive consistency on G: G(t+u)+G(t-u)=P(G(t),G(u)). The Recognition Composition Law supplies the exact form of P used in the hypothesis.
proof idea
The term proof introduces t and u, simplifies the goal with the definition of H_of, applies the log_consistency lemma to obtain the additive relation on G, substitutes the explicit P form via the hPrcl hypothesis, rewrites, and closes the equality with linarith.
why it matters in Recognition Science
This result supplies the direct implication from RCL-style consistency to d'Alembert on the log-lift and is invoked by the full analytic_bridge_full theorem. It realizes the module's central claim that the RCL combiner leaves no third option between additive and d'Alembert forms. In the framework it sits between the J-uniqueness step (T5) and the derivation of wave equations in the eight-tick octave.
scope and limits
- Does not derive the specific RCL form of P from interaction axioms.
- Does not apply when the combiner P differs from 2uv+2u+2v.
- Does not establish existence or smoothness of F.
- Does not extend the equation to complex arguments or higher dimensions.
formal statement (Lean)
621theorem analytic_bridge (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
622 (hNorm : F 1 = 0)
623 (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
624 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
625 (hPrcl : ∀ u v, P u v = 2 * u * v + 2 * u + 2 * v) :
626 ∀ t u : ℝ, H_of F (t + u) + H_of F (t - u) = 2 * H_of F t * H_of F u := by
proof body
Term-mode proof.
627 intro t u
628 simp only [H_of]
629 -- Goal: G_of F (t + u) + 1 + (G_of F (t - u) + 1) = 2 * (G_of F t + 1) * (G_of F u + 1)
630 -- From log_consistency: G(t+u) + G(t-u) = P(G(t), G(u))
631 have hlog := log_consistency F P hCons t u
632 -- hlog: G_of F (t + u) + G_of F (t - u) = P (G_of F t) (G_of F u)
633 -- P(G(t), G(u)) = 2G(t)G(u) + 2G(t) + 2G(u) by hPrcl
634 have hP := hPrcl (G_of F t) (G_of F u)
635 -- hP: P (G_of F t) (G_of F u) = 2 * G_of F t * G_of F u + 2 * G_of F t + 2 * G_of F u
636 -- Combine: G(t+u) + G(t-u) = 2G(t)G(u) + 2G(t) + 2G(u)
637 rw [hP] at hlog
638 -- Need: G(t+u) + 1 + (G(t-u) + 1) = 2(G(t)+1)(G(u)+1)
639 -- LHS = G(t+u) + G(t-u) + 2 = (by hlog) 2G(t)G(u) + 2G(t) + 2G(u) + 2
640 -- RHS = 2(G(t)G(u) + G(t) + G(u) + 1) = 2G(t)G(u) + 2G(t) + 2G(u) + 2
641 linarith
642
643/-- **The Analytic Bridge Theorem (Full Version)**:
644
645 Multiplicative consistency + Structural axioms + Interaction
646 ⟹ d'Alembert for the log-lift.
647
648 This version derives the RCL form from interaction.
649-/