log_zero_bilinear_identity
plain-language theorem explainer
The zero function satisfies the log-bilinear identity with coefficient zero. Researchers classifying continuous solutions to the d'Alembert equation in the Recognition Science pipeline cite this as the trivial endpoint of the algebraic target. The proof is a direct term-mode verification that unfolds the definition and simplifies by ring arithmetic.
Claim. Let $G(x) = 0$ for all real $x$. Then for all real $t,u$, $G(t+u) + G(t-u) = 2G(t) + 2G(u) + 0·G(t)G(u)$.
background
LogBilinearIdentity(G, c) asserts that a function G satisfies the additive relation G(t+u) + G(t-u) = 2G(t) + 2G(u) + c G(t) G(u) for all real t,u. This is the algebraic target left after smoothness and affine-forcing analysis in the generalized d'Alembert setting. The module GeneralizedDAlembert discharges the polynomial-degree restriction on the route-independence combiner by invoking the Aczél–Kannappan classification of continuous solutions to the classical d'Alembert equation, reducing the problem to continuity of the combiner alone.
proof idea
One-line wrapper that applies the ring tactic after introducing the universal quantifiers t and u.
why it matters
This instance completes the zero branch of the classified log-coordinate costs (parabolic, hyperbolic, trigonometric, or zero) that the module assembles for the continuous-combiner version of SatisfiesLawsOfLogic. It sits inside the move that replaces the polynomial-degree-≤-2 hypothesis with mere continuity, feeding the Translation Theorem pipeline while leaving the quartic-log counterexample as the sharpness witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.