Fquad_on_exp
plain-language theorem explainer
The lemma shows that the quadratic log-cost Fquad applied to exp(t) recovers exactly Gquad(t) = t²/2. Researchers building counterexamples to d'Alembert forcing from the mere existence of a combiner P cite this identity to separate the log-lift from additive structure. The proof is a one-line term simplification that unfolds Fquad via Cost.F_ofLog and cancels log(exp t) = t.
Claim. For every real $t$, if $F(x) := G(Real.log x)$ with $G(t) := t^2/2$, then $F(Real.exp t) = t^2/2$.
background
The module documents that the mere existence of a combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not force the d'Alembert structure for the log-lift of F. In particular the quadratic log-cost admits the additive combiner P(u,v) := 2u + 2v, yet its shifted log-lift H(t) := F(exp t) + 1 does not satisfy the d'Alembert equation; any forcing theorem therefore requires an extra nondegeneracy axiom.
proof idea
The proof is a term-mode simplification that applies the definitions of Fquad and Gquad together with the upstream Cost.F_ofLog unfolding. It relies on the built-in rule Real.log (Real.exp t) = t to equate both sides directly to t²/2.
why it matters
This identity is invoked by the downstream lemmas calib_Fquad (second derivative at zero) and Hquad_simp (explicit form of the shifted lift). It supplies the concrete quadratic counterexample that demonstrates the structural obstruction: the weak ∃P hypothesis alone cannot force the Recognition Composition Law or the J-uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.