Hquad_simp
plain-language theorem explainer
The lemma establishes that the shifted quadratic log-lift equals t squared over 2 plus 1. Researchers constructing counterexamples to forcing the d'Alembert equation from weak combiner existence would cite this simplification. The proof is a one-line simp wrapper that unfolds the relevant definitions of the quadratic cost and its exponential composition.
Claim. Let $H(t) := F(e^t) + 1$ where $F(x) = (log x)^2 / 2$. Then $H(t) = t^2 / 2 + 1$.
background
In this module the quadratic log-cost F is defined by F(x) = (log x)^2 / 2. The upstream lemma states that F(exp t) equals G(t) where G(t) = t^2 / 2. The shifted log-lift H is then defined as F(exp t) + 1. The module documents a simple but important fact: the mere existence of some combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) does not force the d'Alembert structure for the log-lift of F. In particular the quadratic case admits the additive combiner P(u, v) = 2u + 2v but its shifted log-lift H does not satisfy the d'Alembert equation. This is a structural obstruction requiring additional nondegeneracy axioms for any forcing theorem.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of the shifted lift, the exponential composition relation, and the explicit quadratic form. The tactic reduces the left side by direct substitution of these three facts.
why it matters
This identity is used by the theorem showing that the shifted quadratic log-lift fails the d'Alembert identity H(t + u) + H(t - u) = 2 H(t) H(u). It contributes to the module's demonstration that existence of a combiner does not imply the Recognition Composition Law on the log-lift. In the framework this underscores the necessity of the full forcing chain from T0 to T8 rather than weak existence hypotheses alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.