Hquad_not_dAlembert
plain-language theorem explainer
The quadratic log-lift H(t) = t²/2 + 1 fails to satisfy the d'Alembert functional equation. Researchers working on forcing the Recognition Composition Law from weak combiner hypotheses would cite this counterexample. The proof assumes the conjunction of H(0) = 1 and the d'Alembert identity, specializes to t = u = 1, and derives an immediate numerical contradiction between 4 and 9/2 via the explicit form of H.
Claim. Let $H(t) = t^2/2 + 1$. Then it is not the case that $H(0) = 1$ and $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t, u$.
background
The module supplies counterexamples showing that the mere existence of a 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. Here Fquad is the quadratic log-cost F(x) = (log x)^2 / 2, which admits the additive combiner P(u, v) = 2u + 2v. The shifted log-lift is defined by Hquad(t) := Fquad(exp t) + 1, which simplifies to the explicit quadratic H(t) = t²/2 + 1 by the sibling lemma Hquad_simp. This setting isolates a structural obstruction: any claim that ∃P alone implies the Recognition Composition Law must add further nondegeneracy axioms.
proof idea
The tactic proof assumes the conjunction, extracts the d'Alembert identity, and specializes it at t = 1, u = 1. It then computes the left side Hquad(2) + Hquad(0) by applying Hquad_simp followed by norm_num to obtain 4, and the right side 2 Hquad(1) Hquad(1) by simp and ring to obtain 9/2. A short calc chain equates the two sides under the assumption and closes with norm_num to produce the contradiction.
why it matters
This result shows that weak existence of a combiner P is insufficient to recover the d'Alembert form required for the Recognition Composition Law. It is invoked directly by the sibling theorem Fquad_not_dAlembert_structure in the FourthGate module and by the duplicate Hquad_not_dAlembert there. Within the Recognition Science framework it supplies the concrete obstruction that forces the addition of nondegeneracy conditions before the forcing chain (T0–T8) can reach J-uniqueness, the phi fixed point, and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.