analytic_bridge

formal source

 618    The key insight is that when P is the RCL combiner, the log-consistency
 619    equation directly implies the d'Alembert functional equation.
 620-/
 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
 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-/
 650theorem analytic_bridge_full (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
 651    (hNorm : F 1 = 0)