calib_Fquad
plain-language theorem explainer
The lemma shows that the second derivative at zero of the composition of the quadratic log-cost F with the exponential equals one. Researchers examining functional equations and counterexamples in Recognition Science cite it to calibrate the curvature of the quadratic case. The proof first reduces the composition to t squared over two via simplification lemmas, then applies the power rule to obtain the first derivative as the identity, and finally evaluates the derivative of the identity at zero.
Claim. Let $F(x) = (1/2) (log x)^2$. Then the second derivative at zero of the map $t mapsto F(e^t)$ equals 1.
background
In this module the quadratic log-cost is introduced as Fquad, defined via Cost.F_ofLog applied to Gquad where Gquad(t) equals t squared over two. The supporting lemma Fquad_on_exp states that Fquad composed with the exponential recovers Gquad exactly, so the composition simplifies to t squared over two. The module documentation explains that this F admits the additive combiner P(u,v) equals 2u plus 2v, yet the shifted log-lift fails the d'Alembert equation, showing that mere existence of some combiner does not force the Recognition Composition Law structure.
proof idea
The tactic proof first uses funext and simplification with Fquad_on_exp and Gquad to establish that the composition equals the function sending t to t squared over two. It then proves the first derivative of that quadratic is the identity function by applying the power rule via HasDerivAt.fun_pow, dividing by the constant two, and simplifying the coefficient. Finally it rewrites the second derivative and evaluates the derivative of the identity function at zero to obtain the value one.
why it matters
This lemma supplies the explicit curvature calibration for the quadratic counterexample inside the module that documents the structural obstruction: existence of a combiner P satisfying F(xy) plus F(x/y) equals P(F(x),F(y)) does not force the d'Alembert form on the log-lift. It therefore supports the module's conclusion that any theorem claiming to derive the Recognition Composition Law from a weak existence hypothesis must add at least one further nondegeneracy axiom. In the broader framework the result underscores the gap between the weak combiner hypothesis and the full T5 J-uniqueness plus RCL steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.