quartic_second_derivative
The second derivative of the map t ↦ t^4 equals the map t ↦ 12 t^2. Workers on obstructions to continuous combiners cite the identity to exclude the quartic from satisfying the Aczel second-derivative relation. The proof is a direct term-mode calculation that invokes the power rule twice and finishes with polynomial simplification.
claim$d^2/dt^2 (t^4) = 12 t^2$
background
The module examines second derivatives to test candidate functions against the continuous-combiner route. The quartic G(t) = t^4 is the finite-polynomial-closure counterexample already used in the paper; it satisfies G''(0) = 0 yet G''(1) = 12, so no function ψ can obey 2 G''(t) = ψ(G t) · G''(0) for all t. The local setting is therefore the obstruction that blocks proof of the residual input continuous_combiner_second_derivative_identity from the standing hypotheses.
proof idea
The term proof begins with funext t to obtain pointwise equality. It rewrites the first derivative via the power rule to 4 t^3, then applies norm_num on deriv_const_mul and deriv_pow to reach the second derivative 12 t^2, and closes with ring.
why it matters in Recognition Science
The theorem supplies the explicit second derivative required by the downstream result quartic_not_aczel_second_derivative_identity, which concludes that the quartic fails AczelSecondDerivativeIdentity. It thereby fills the counterexample slot in the second-derivative obstruction for the continuous-combiner route. The identity supports the broader claim that the quartic cannot serve as a solution inside the forcing chain leading to the Recognition Composition Law.
scope and limits
- Does not establish the identity for any function other than the quartic.
- Does not derive or negate the Aczel identity itself.
- Does not construct or refute the continuous combiner.
- Does not treat higher-order derivatives or other polynomial degrees.
Lean usage
rw [quartic_second_derivative] at h1formal statement (Lean)
22private theorem quartic_second_derivative :
23 deriv (deriv (fun t : ℝ => t^4)) = fun t => 12*t^2 := by
proof body
Term-mode proof.
24 funext t
25 rw [show deriv (fun t : ℝ => t^4) = fun t => 4*t^3 by
26 funext x
27 norm_num [deriv_pow]]
28 rw [show deriv (fun t : ℝ => 4*t^3) t = 4 * (3*t^2) by
29 norm_num [deriv_const_mul, deriv_pow]]
30 ring
31