Fquad_on_exp
plain-language theorem explainer
The lemma equates the quadratic cost Fquad applied to exp t with the explicit quadratic Gquad at t. Researchers constructing counterexamples to d'Alembert forcing from weak combiner existence cite this identity to relate the log-lifted cost to its G form. The proof is a one-line term simplification that unfolds the log-lift definition and substitutes the quadratic expression.
Claim. Let $F(x) := G(Real.log x)$ where $G(t) := t^2 / 2$. Then $F(Real.exp t) = G(t)$ for all real $t$.
background
The module exhibits a structural obstruction: existence of a combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not force the d'Alembert equation on the log-lift. Here the quadratic log-cost is realized explicitly as Fquad := F_ofLog Gquad with Gquad(t) := t^2 / 2, so Fquad(x) = (log x)^2 / 2. This F admits the additive combiner P(u, v) := 2u + 2v, yet the shifted lift H(t) := Fquad(exp t) + 1 fails to satisfy d'Alembert.
proof idea
Term-mode proof consisting of a single simp that unfolds Fquad to Cost.F_ofLog Gquad, applies the definition of F_ofLog, and reduces via the explicit form of Gquad together with the identity log(exp t) = t.
why it matters
The identity supports the calibration step in calib_Fquad and the simplification in Hquad_simp, both of which rely on Fquad(exp t) = Gquad t to identify the explicit quadratic form of the shifted lift. It fills the module's role of documenting that weak combiner existence fails to imply the Recognition Composition Law or d'Alembert structure, requiring additional nondegeneracy axioms. The construction directly illustrates the obstruction described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.