log_consistency
If a cost function F obeys multiplicative consistency F(xy) + F(x/y) = P(Fx, Fy) for positive arguments, then its log-lift G(t) = F(exp t) obeys the corresponding additive relation G(t+u) + G(t-u) = P(Gt, Gu). Recognition Science authors cite this when moving from multiplicative interaction axioms to additive functional equations on the log scale. The proof is a direct substitution that replaces the arguments of F by exponentials and invokes the addition formulas for exp.
claimLet $F : (0,∞) → ℝ$ and $P : ℝ → ℝ → ℝ$. If $F(xy) + F(x/y) = P(F(x), F(y))$ holds for all $x,y > 0$, then the log-lift $G(t) := F(e^t)$ satisfies $G(t+u) + G(t-u) = P(G(t), G(u))$ for all real $t,u$.
background
The AnalyticBridge module proves that structural axioms on a cost function plus an interaction combiner force the d'Alembert functional equation on the log-lift. The log-lift is defined by G_of F t := F(exp t), which converts the multiplicative consistency hypothesis into an additive one. Upstream results supply the reparametrization G in Cost.FunctionalEquation and the gravitational constant G in Constants, both of which appear as sibling or imported definitions of the same log-coordinate change.
proof idea
The term proof introduces t and u, unfolds the definition of G_of, records that exp t and exp u are positive, applies the given consistency hypothesis, rewrites the products and quotients via exp_add and exp_sub, then converts the resulting equality by rewriting the remaining exp_add and exp_sub terms.
why it matters in Recognition Science
log_consistency is invoked by analytic_bridge, Q_boundary_v, Q_boundary_u, entangling_combiner_forces_hyperbolic and separable_combiner_forces_flat. It supplies the precise translation step that lets the module's strategy (differentiate the consistency equation, constrain the combiner Q, force the d'Alembert form) proceed from the multiplicative hypothesis to the additive d'Alembert equation. The result therefore closes one link in the chain from Recognition Composition Law to the eight-tick octave and D=3.
scope and limits
- Does not assume any concrete form for the combiner P.
- Does not derive the d'Alembert equation or the ODE G'' = G + 1.
- Does not impose differentiability or continuity on F.
- Does not reference physical constants, dimensions or the phi-ladder.
formal statement (Lean)
55theorem log_consistency (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
56 (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
57 ∀ t u : ℝ, G_of F (t + u) + G_of F (t - u) = P (G_of F t) (G_of F u) := by
proof body
Term-mode proof.
58 intro t u
59 simp only [G_of]
60 have hpos_t : 0 < Real.exp t := Real.exp_pos t
61 have hpos_u : 0 < Real.exp u := Real.exp_pos u
62 have h := hCons (Real.exp t) (Real.exp u) hpos_t hpos_u
63 simp only [Real.exp_add, Real.exp_sub] at h
64 convert h using 2
65 · rw [Real.exp_add]
66 · rw [Real.exp_sub]
67
68/-! ## Boundary Conditions on Q (= P) -/
69
70/-- From normalization F(1) = 0, we get G(0) = 0. -/