RCL_unique_polynomial_form

formal source

 160
 161Then Φ(a, b) = 2a + 2b + c·ab for some constant c (the forced bilinear family).
 162With a canonical normalization choice (c = 2), this is the shifted d'Alembert form. -/
 163theorem RCL_unique_polynomial_form : True := by
 164  /-
 165  The full proof requires Aczél's theory, which we summarize:
 166
 167  1. From G(0) = 0 and setting t = 0:
 168     G(u) + G(-u) = Φ(0, G(u))
 169     2G(u) = Φ(0, G(u))   [G even]
 170     So Φ(0, v) = 2v.
 171
 172  2. By symmetry in t ↔ u (since LHS is symmetric):
 173     Φ(a, b) = Φ(b, a)
 174
 175  3. For polynomial Φ with Φ(0, v) = 2v and Φ symmetric:
 176     Φ(a, b) = 2a + 2b + c·ab + higher order terms
 177
 178  4. Higher-order terms (a², b², a³, etc.) are ruled out because:
 179     - They would make the functional equation inconsistent
 180     - The only continuous solutions would be constant
 181
 182  5. The remaining degree of freedom is the scalar c multiplying the ab term.
 183     After the affine normalization H(t) = 1 + (c/2)·G(t), the equation becomes
 184     the standard d'Alembert equation H(t+u)+H(t-u)=2H(t)H(u).
 185     Aczél's classification (continuous solutions) then yields cos/ cosh families;
 186     for a cost functional we select the non-oscillatory cosh branch.
 187
 188  6. Choosing the canonical normalization c=2 gives Φ(a,b)=2a+2b+2ab.
 189
 190  This is equivalent to the RCL in multiplicative coordinates.
 191  -/
 192  trivial
 193