quadraticWitness_not_coshAdd
plain-language theorem explainer
The quadratic cost G(t)=t²/2 fails the Cosh-Add (d'Alembert) identity on the log axis. Anyone citing the T5 no-go needs this elementary counterexample: at t=u=1 one gets LHS=2 and RHS=5/2. The proof is a one-point instantiation plus numeric simplification.
Claim. The quadratic witness $G(t)=t^2/2$ does not satisfy the Cosh-Add identity $G(t+u)+G(t-u)=2G(t)G(u)+2(G(t)+G(u))$ for all real $t,u$. In particular the identity fails at $t=u=1$, where the left-hand side is $2$ and the right-hand side is $5/2$.
background
The module derives two T5 constraints from ledger structure (T3): reciprocal symmetry $F(x)=F(1/x)$ from double-entry bookkeeping, and unit normalization $F(1)=0$ from the identity posting. It then proves a no-go: those constraints plus continuity and unit log-curvature do not force the remaining T5 ingredient.
Cosh-Add (the log-axis form of composition law C6) asks that a reparametrized cost $G:\mathbb{R}\to\mathbb{R}$ obey $G(t+u)+G(t-u)=2G(t)G(u)+2(G(t)+G(u))$ for all real $t,u$. This is the d'Alembert-type identity used in the Aczél-style classification that yields $J(x)=\frac12(x+1/x)-1$. The quadratic witness $G(t)=t^2/2$ is the standard counterexample family member: even, zero at the origin, smooth, with unit second derivative at zero, yet not Cosh-Add.
Upstream, $G$ also appears as the log-coordinate reparametrization $G_F(t)=F(e^t)$ in the cost functional-equation layer; here the name is reused for a concrete test function on the additive line.
proof idea
Assume Cosh-Add holds for the quadratic witness. Specialize to $t=u=1$. Unfold $G(t)=t^2/2$ and reduce both sides by norm_num: left-hand side is $G(2)+G(0)=2+0=2$; right-hand side is $2\cdot G(1)\cdot G(1)+2(G(1)+G(1))=2\cdot(1/2)\cdot(1/2)+2(1/2+1/2)=1/2+2=5/2$. Contradiction. No continuity or curvature lemmas are needed; the single point $(1,1)$ already kills the universal quantifier.
why it matters
This lemma is the computational heart of aczel_hypothesis_refuted, the module's NO-GO certificate resolving internal Finding 2. That parent theorem shows the retained proposition "evenness + unit + continuity + unit log-curvature force Cosh-Add" is false, by feeding the quadratic witness through the four side conditions and then invoking this non-identity.
In the Recognition forcing chain, T5 claims uniqueness of $J(x)=\cosh(\log x)-1$ (equivalently $\frac12(x+x^{-1})-1$) among admissible costs. The honest dependency diagram in the module doc makes C6 an independent, load-bearing hypothesis: ledger structure forces only symmetry and unit; composition is not free. Without this counterexample the earlier (retracted) claim that T5 follows unconditionally from T1–T4 would stand. The result therefore keeps the T5 characterization honest: RCL/Cosh-Add must be postulated, not derived from double-entry alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.