log_consistency
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.