Hquad
plain-language theorem explainer
Hquad defines the shifted log-lift of the quadratic log-cost by composing Fquad with the exponential map and adding one. Researchers constructing counterexamples to weak forcing of d'Alembert equations from an arbitrary combiner P would cite this object. The definition is a direct composition that immediately yields the explicit quadratic form t squared over 2 plus 1.
Claim. Let $F(x) = (1/2) (log x)^2$ be the quadratic log-cost. The shifted log-lift is $H(t) := F(e^t) + 1$.
background
The module documents that existence of some combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not force the d'Alembert structure on the log-lift of F. The quadratic log-cost F(x) := (log x)^2 / 2 admits the additive combiner P(u,v) := 2u + 2v, yet its shifted log-lift H(t) := F(exp t) + 1 fails the d'Alembert equation. Fquad is obtained as Cost.F_ofLog Gquad, supplying the explicit quadratic in the log domain.
proof idea
The definition is a one-line wrapper that applies Fquad to exp t and adds the constant 1.
why it matters
Hquad supplies the concrete quadratic counterexample that feeds the theorem Hquad_not_dAlembert and the simplification lemma Hquad_simp. It demonstrates the module's central claim that any theorem forcing the Recognition Composition Law from a weak ∃P hypothesis must add further nondegeneracy axioms. In the framework this illustrates why the full T0-T8 forcing chain is required rather than a minimal existence assumption on P.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.