Hquad_not_dAlembert
plain-language theorem explainer
The quadratic log-lift H(t) = t²/2 + 1 fails the d'Alembert functional equation. Researchers classifying admissible cost functions in Recognition Science cite this counterexample to exclude quadratic candidates from the phi-ladder. The proof assumes the structure, specializes the identity at t=1 and u=1, and reaches a numerical contradiction by normalization.
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 Fourth Gate module encodes the d'Alembert structure on the shifted log-lift of a cost function. SatisfiesDAlembert H is the proposition that H(0) = 1 and the classical identity H(t+u) + H(t-u) = 2 H(t) H(u) holds for all real t and u. Continuous solutions are exactly the functions cosh(λ t). In the Recognition Science setting this gate is a derived consequence of the curvature ODE from Gate 3 once evenness and calibration are imposed, forcing the hyperbolic form tied to J-uniqueness.
proof idea
The proof is a one-line wrapper. It introduces the assumption that SatisfiesDAlembert holds, extracts the functional-equation conjunct, specializes at t=1 and u=1, and applies norm_num to obtain an immediate numerical falsehood.
why it matters
This result excludes the quadratic log-lift as a possible cost function and feeds directly into Fquad_not_dAlembert_structure. It closes a loophole in the classification of functions satisfying the d'Alembert gate, reinforcing that only the hyperbolic branch (linked to T5 J-uniqueness and the eight-tick octave) survives the forcing chain to D=3. The theorem therefore supports the uniqueness claim for the admissible cost functions in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.