quadraticWitness_zero
plain-language theorem explainer
The quadratic witness $G(t)=t^2/2$ vanishes at the origin: $G(0)=0$. Anyone citing the T5 no-go certificate (that ledger symmetry, unit, continuity, and unit curvature do not force Cosh-Add) needs this elementary normalization fact. The proof is a one-line simplification of the definition.
Claim. Let $G:\mathbb{R}\to\mathbb{R}$ be the quadratic cost witness $G(t)=t^2/2$. Then $G(0)=0$.
background
This module sits in the T5 verification layer of Recognition Science. From the ledger (T3) it derives reciprocal symmetry $F(x)=F(1/x)$ and unit normalization $F(1)=0$, then proves a no-go: those constraints plus continuity and unit log-curvature do not force the Cosh-Add (d'Alembert) identity that completes the T5 characterization of $J$.
The counterexample is the quadratic witness $G(t)=t^2/2$. Upstream, that function is defined as a plain real map; the doc-comment records that it is even, vanishes at $0$, continuous, and has unit second derivative at the origin, yet fails Cosh-Add. The present lemma is the vanishing-at-zero half of that checklist.
proof idea
One-line wrapper: unfold the definition $G(t)=t^2/2$ by simp and evaluate at $0$, which yields $0$ immediately.
why it matters
Feeds the kernel-checked no-go theorem aczel_hypothesis_refuted, which discharges Finding 2 of the 2026 internal audit. That theorem applies the Aczél-style hypothesis package to $G$ and obtains a contradiction via the separate fact that $G$ fails Cosh-Add; the package requires evenness, $G(0)=0$, continuity, and unit second derivative. Without $G(0)=0$, the witness would not be admissible under the stated hypotheses.
In the honest forcing chain, T3 yields symmetry and unit, while composition law C6 remains an independent load-bearing hypothesis of T5 ($J(x)=\frac12(x+x^{-1})-1$). This lemma is a tiny but mandatory step in making that independence machine-checked rather than rhetorical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.