Fquad
plain-language theorem explainer
Fquad defines the quadratic log-cost F(x) = (log x)^2 / 2 on positive reals. Researchers studying functional equations for cost functions cite it as a counterexample showing that an additive combiner P(u,v) = 2u + 2v satisfies weak consistency without forcing d'Alembert structure on the shifted lift. The definition is a direct composition of the log-lift operator with the quadratic Gquad.
Claim. $F(x) := (log x)^2 / 2$ for $x > 0$.
background
The module documents that existence of some combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not force d'Alembert structure on the log-lift of F. The quadratic log-cost admits the additive combiner P(u,v) := 2u + 2v, yet its shifted lift H(t) := F(exp t) + 1 does not satisfy the d'Alembert equation. This shows a structural obstruction requiring extra nondegeneracy axioms beyond the weak hypothesis.
proof idea
One-line definition applying the log-lift operator Cost.F_ofLog to Gquad(t) := t^2 / 2.
why it matters
This definition supplies the quadratic counterexample feeding lemmas such as Fquad_consistency (verifying weak consistency with the additive combiner) and Fquad_on_exp (relating values back to Gquad). It illustrates the module's core point that weak existence of P alone does not imply the Recognition Composition Law. In the framework it underscores the need for further conditions to reach the RCL form involving J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.