quartic_second_derivative
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.