Fquad_on_exp
plain-language theorem explainer
The lemma shows that the quadratic log-cost Fquad applied to exp(t) recovers Gquad(t) = t²/2 exactly. Counterexample work in the d'Alembert module cites this identity to compare the log-lifted H with its G form. The proof is a one-line simplification that unfolds F_ofLog and substitutes the explicit quadratic.
Claim. For all real $t$, $F(e^{t}) = t^{2}/2$ where $F(x) := (log x)^{2}/2$.
background
The module documents that existence of some combiner P with F(xy) + F(x/y) = P(F(x), F(y)) does not force the d'Alembert equation on the log-lift H(t) = F(exp t) + 1. Fquad is defined by Cost.F_ofLog Gquad, where F_ofLog G (x) := G(log x) and Gquad(t) := t²/2, so Fquad(x) = (log x)²/2. This quadratic admits the additive combiner P(u,v) := 2u + 2v yet its shifted lift fails d'Alembert, showing a structural obstruction that requires an extra nondegeneracy axiom.
proof idea
One-line wrapper that applies simp on the definitions of Fquad, Cost.F_ofLog, and Gquad, using that log(exp t) = t.
why it matters
The identity is invoked by calib_Fquad (to evaluate second derivatives at 0) and by Hquad_simp (to obtain the explicit form of the shifted lift). It fills the module's role of exhibiting a concrete counterexample that any forcing theorem from weak ∃P must add further axioms. The quadratic Gquad is contrasted with the hyperbolic G of the RCL in the CurvatureGate sibling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.