quadraticWitness
plain-language theorem explainer
Defines the quadratic cost witness $G(t)=t^2/2$ on the reals. Anyone citing the T5 ledger no-go uses it: the map is even, vanishes at zero, continuous, and has unit second derivative at the origin, yet fails Cosh-Add. The body is a one-line function definition.
Claim. Let $G:\mathbb{R}\to\mathbb{R}$ be the quadratic cost witness $G(t)=t^2/2$.
background
Module Verification.T5.LedgerCost 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 ledger facts plus continuity and unit log-curvature calibration do not force the Cosh-Add (d'Alembert) identity that finishes the T5 classification of $J$.
Cosh-Add is the composition law C6 in the Aczél-type chain that yields the unique admissible cost $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$). An earlier draft claimed C6 followed from ledger constraints via Aczél (1966, Thm. 3.1.3); that claim is retracted. The counterexample is this quadratic witness.
proof idea
Pure definition: the noncomputable map sending each real $t$ to $t^2/2$. No proof obligations. Downstream lemmas discharge the witness properties by unfolding this definition (evenness by simp, continuity by fun_prop, first derivative via HasDerivAt of $t\mapsto t^2/2$, second derivative at $0$ equal to $1$, and failure of Cosh-Add by evaluating at $(1,1)$).
why it matters
This is the concrete counterexample behind the module's main result aczel_hypothesis_refuted (Finding 2 resolution): symmetry, unit, continuity, and unit second-derivative calibration do not force Cosh-Add. The composition law C6 is therefore an independent, load-bearing hypothesis of the T5 characterization, not a ledger corollary.
Downstream, the witness feeds the property lemmas (even, zero at origin, continuous, first and second derivatives) and quadraticWitness_not_coshAdd (LHS $2$ vs RHS $5/2$ at $t=u=1$), which together refute the Aczél-style hypothesis package. In the forcing chain this keeps T5 honest: $J$-uniqueness still needs RCL/Cosh-Add as a separate axiom, not something T3 alone supplies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.