Hquad_simp
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not show that the shifted quadratic log-lift satisfies d'Alembert.
- Does not apply to costs other than the quadratic log-cost.
- Does not establish the existence or form of the combiner P.
- Does not involve the self-similar fixed point phi or the eight-tick octave.
formal statement (Lean)
98lemma Hquad_simp (t : ℝ) : Hquad t = t ^ 2 / 2 + 1 := by
proof body
One-line wrapper that applies simp.
99 simp [Hquad, Fquad_on_exp, Gquad]
100