Fquad_unit0
plain-language theorem explainer
The lemma shows that the quadratic log-cost evaluates to zero at the multiplicative unit. Counterexample work on forcing d'Alembert from mere existence of a combiner P cites this evaluation to fix the quadratic case. The proof is a one-line simplification that unfolds Fquad via F_ofLog and Gquad.
Claim. Let $G(t) := t^2/2$ and $F(x) := G(Real.log x)$. Then $F(1) = 0$.
background
The module records that existence of some combiner P with F(xy) + F(x/y) = P(F(x), F(y)) does not force d'Alembert structure on the log-lift. Gquad is defined by Gquad(t) := t²/2 and Fquad by Fquad(x) := Cost.F_ofLog Gquad, which expands to Gquad(Real.log x). Upstream F_ofLog supplies the lift from the additive line to the multiplicative line.
proof idea
One-line wrapper that applies simp with the definitions of Fquad, F_ofLog, and Gquad.
why it matters
The lemma fixes the base case for the quadratic counterexample that demonstrates the structural obstruction: any claim forcing RCL/d'Alembert from ∃P requires an extra nondegeneracy axiom. It sits inside the module that contrasts the quadratic G with the hyperbolic G of the RCL and records the need for that axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.