bilinear_family_reduction
plain-language theorem explainer
Any cost functional obeying a bilinear multiplicative consistency relation reduces to the standard d'Alembert equation after the affine redefinition H(t) = 1 + (c/2) F(exp t). Functional equation specialists in the Recognition Science program cite this reduction to link the general family to the RCL form. The argument is a direct algebraic verification that substitutes the exponential variables and matches coefficients via ring simplification.
Claim. Suppose $F : (0,∞) → ℝ$ satisfies $F(xy) + F(x/y) = 2F(x) + 2F(y) + c F(x)F(y)$ for all $x,y > 0$ and some constant $c ≠ 0$. Let $G(t) := F(e^t)$. Then the shifted function $H(t) := 1 + (c/2) G(t)$ obeys the d'Alembert functional equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$.
background
This module shows that multiplicative consistency for cost functionals forces a bilinear form, which then reduces to d'Alembert. A cost functional $F$ maps positive reals to reals and obeys symmetry $F(x) = F(1/x)$ together with normalization $F(1) = 0$. The consistency condition is $F(xy) + F(x/y) = P(F(x), F(y))$ where $P$ is a symmetric quadratic polynomial; the module proves $P$ must take the bilinear shape $2u + 2v + c uv$ for some $c$ (see sibling results on polynomial_form_forced and symmetry_and_normalization_constrain_P).
proof idea
The proof introduces the exponential reparametrization $G(t) = F(exp t)$ and the affine shift $H(t) = 1 + (c/2) G(t)$. It substitutes $x = exp t$, $y = exp u$ into the bilinear hypothesis, rewrites the target identity in terms of $F(xy)$ and $F(x/y)$, applies the hypothesis, and verifies the resulting algebraic identity by ring arithmetic (using exp_add and exp_sub for the change of variables).
why it matters
This lemma supplies the reduction step that converts the bilinear family forced by consistency into the classical d'Alembert equation. It feeds the main theorem of the module that recovers the Recognition Composition Law once $c = 2$ is fixed by normalization. In the framework it connects J-uniqueness (T5) to the RCL form $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ via the upstream shift $H = J + 1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.