log_consistency_of_mult_consistency
plain-language theorem explainer
The theorem shows that multiplicative consistency of F on positive reals transfers directly to additive consistency of its log-reparametrized version G. Researchers deriving the Recognition Composition Law from first principles would cite this reduction when moving from the original F-equation to d'Alembert form. The proof is a direct substitution that replaces arguments with exponentials and applies the addition formulas for exp.
Claim. Let $F : (0,∞) → ℝ$ and $P : ℝ → ℝ → ℝ$ satisfy $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x,y > 0$. Define $G(t) := F(e^t)$. Then $G(t+u) + G(t-u) = P(G(t), G(u))$ for all real $t,u$.
background
The Full Unconditional module derives both F and P from multiplicative consistency plus normalization, symmetry, and smoothness, with no prior assumption on P. The reparametrization G(t) = F(exp t) converts the multiplicative relation F(xy) + F(x/y) = P(F(x), F(y)) into an additive one. LogConsistency is the resulting statement: ∀ t u, G(t+u) + G(t-u) = Q(G(t), G(u)). Upstream, the G reparametrization appears in Cost.FunctionalEquation as the standard change of variables that turns the Recognition Composition Law into d'Alembert form.
proof idea
The proof is a one-line term-mode wrapper. It introduces t and u, applies the definition of G to obtain F(exp t) and F(exp u), invokes the hypothesis on these positive arguments, and rewrites the products and quotients via the identities exp(t+u) = exp t · exp u and exp(t-u) = exp t / exp u.
why it matters
This step converts the given multiplicative consistency into the log-additive equation required for the ODE analysis that forces F to equal J and P to the bilinear form. It supports the module's claim that both F and P are uniquely determined without assuming any structure on P. In the Recognition Science chain this reduction is the bridge from the original RCL hypothesis to the d'Alembert equation used in the full unconditional theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.