Fquad_not_dAlembert_structure
plain-language theorem explainer
The quadratic cost function fails the d'Alembert structure condition on its shifted log-lift. Researchers completing the Recognition Science four-gate argument cite this to exclude quadratic solutions. The proof assumes the structure holds, equates the lift to the explicit quadratic form via substitution, and reduces directly to the negation theorem for that form.
Claim. Let $F$ be the cost function obtained as the log-lift of $G(t) = t^2/2$. Then the shifted function $H(t) = F(e^t) + 1$ does not satisfy the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ together with $H(0) = 1$.
background
The Fourth Gate checks whether a cost function satisfies d'Alembert structure, meaning its shifted log-lift $H(t) = F(e^t) + 1$ obeys the classical functional equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0)=1$. This module presents the gate as a derived cross-check after the curvature gate, where the hyperbolic solution automatically satisfies it. The quadratic counterexample is constructed as the log-lift of $G(t) = t^2/2$, and the direct negation for its $H$ is established upstream.
proof idea
Assume the d'Alembert structure for the quadratic cost function. Unfold the definition to obtain the functional equation for the shifted lift. Substitute the explicit form $t^2/2 + 1$ obtained from the log-lift definition and the quadratic $G$. Apply the upstream theorem that directly negates the equation for this quadratic lift.
why it matters
This result is invoked in the fourth gate summary to pair the positive result for Jcost with the negative for the quadratic, and in the gates consistent theorem to show uniform distinction across all four gates. It supplies the d'Alembert exclusion that completes the chain selecting the J-cost, consistent with J-uniqueness and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.