hasDerivAt_rpow_two
plain-language theorem explainer
The lemma establishes that the squaring map has derivative 2r at r. Analysts formalizing Navier-Stokes estimates cite it when differentiating quadratic radial factors inside integration-by-parts identities. The proof is a one-line term that applies the power rule to the derivative of the identity function.
Claim. For every real number $r$, the function $xmapsto x^2$ is differentiable at $r$ with derivative $2r$.
background
The SkewHarmGate module supports analytic steps for the Navier-Stokes equations, specifically skew/self-adjoint cancellations obtained from integration by parts without bad boundary terms and harmonic/affine tail bookkeeping where the sole obstruction is a boundary term at infinity. This lemma supplies the derivative of the quadratic radial factor that appears repeatedly in those identities. It depends on the upstream pow lemma from RecogSpec.Core, which states that if $x$ is PhiClosed then $x^n$ remains PhiClosed.
proof idea
The proof is a term-mode one-liner. It invokes the power rule on the derivative of the identity function at $r$ and reduces via simpa to the required HasDerivAt statement for the squaring map.
why it matters
The lemma is invoked by hasDerivAt_rsq_mul to obtain the product rule for $(t^2)A'(t)$ and by zeroSkewAtInfinity_of_integrable to control integrable skew terms. It supplies the differentiation step required for the skew cancellations described in the module documentation for navier-dec-12-rewrite.tex. In the Recognition framework it contributes to the analytic machinery supporting $D=3$ in the unified forcing chain T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.