quadraticWitness_deriv
plain-language theorem explainer
The first derivative of the quadratic witness G(t)=t²/2 is the identity map t ↦ t on ℝ. Anyone checking the curvature calibration of the T5 no-go witness cites this. The argument is a short differentiation via the power rule, rewritten under funext.
Claim. Let $G:\mathbb{R}\to\mathbb{R}$ be given by $G(t)=t^2/2$. Then $\frac{d}{dt}G(t)=t$ pointwise, i.e. $\mathrm{deriv}(G)$ equals the identity function on $\mathbb{R}$.
background
This module extracts two T5 cost constraints from ledger structure (T3): reciprocal symmetry F(x)=F(1/x) from double-entry, and unit normalization F(1)=0 from the identity posting. It also proves a no-go: those ledger facts plus continuity and curvature calibration do not force the Cosh-Add (d'Alembert) composition law. The composition law remains an independent load-bearing hypothesis of the T5 uniqueness theorem for J.
The quadratic witness is the explicit counterexample G(t)=t²/2. By design it is even, vanishes at 0, is continuous, and has unit second derivative at the origin, yet it fails Cosh-Add. Establishing its first derivative is the intermediate calculus step needed before reading off that second-derivative calibration.
In the broader Recognition chain, T5 asserts uniqueness of J(x)=(x+x⁻¹)/2−1 (equivalently cosh(log x)−1) among admissible costs. The ledger alone cannot force that form; the witness separates ledger-derived constraints from the composition law.
proof idea
Pointwise via funext. For each x one builds HasDerivAt G x x from the power rule: hasDerivAt_pow 2 x gives the derivative of t ↦ t², then divide by the constant 2. After simp with the definition of G and pow_one, the derivative value is x. HasDerivAt.deriv then yields the pointwise equality, and funext assembles the function equality deriv G = id.
why it matters
Feeds the sibling lemma that the second derivative of G at 0 equals 1, which is the curvature-calibration half of the no-go certificate. That certificate shows symmetry, unit, continuity, and λ=1 calibration do not imply Cosh-Add; the witness violates the identity at t=u=1 (LHS=2, RHS=5/2).
In the honest forcing chain, T3 yields only reciprocal symmetry and F(1)=0. C6 (composition / Cosh-Add) and C7 (calibration) stay independent inputs to the Aczél-type classification that pins T5's unique J. This derivative lemma is a small but necessary calculus brick under that no-go: without the first derivative, the unit-second-derivative check does not go through.
Historically the file once claimed Cosh-Add followed from ledger plus continuity; the 2026 audit retracted that. The quadratic witness and its derivative facts are the kernel-checked refutation path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.