hasDerivAt_affine_quad
plain-language theorem explainer
The real quadratic a + b t + c t² is differentiable at t = 0 with derivative equal to the linear coefficient b. Analysts working the Euclidean weak-field TT first variation of the closed 4D midpoint Bloch symbol cite it as the elementary one-variable calculus step that turns an affine-quadratic expansion along a finite line into a HasDerivAt fact. The proof assembles Mathlib power, scalar-multiply, and sum rules, then rewrites the target function into that sum form.
Claim. For all real coefficients $a,b,c$, the map $t \mapsto a + b t + c t^{2}$ is differentiable at $t = 0$ and its derivative there equals $b$.
background
The ambient module treats the TT directional first variation of the closed 4D midpoint Bloch symbol in the Euclidean weak-field sector. Along a finite line $H + t \cdot K$ in the space of $4\times 4$ matrices, the midpoint symbol expands as an affine-quadratic polynomial in the real parameter $t$. Differentiating that expansion at $t = 0$ is exactly the directional first variation.
HasDerivAt f f' x is Mathlib's pointwise differentiability predicate: $f$ has derivative $f'$ at $x$. The present lemma isolates the pure one-variable calculus fact needed before any matrix or Bloch structure is reintroduced. Module honesty bounds apply only to the parent variation theorems, not to this scalar identity.
proof idea
Four local facts are built, then glued. First, hasDerivAt_pow 2 0 gives that $t \mapsto t^{2}$ has derivative $0$ at $0$. Constant-multiply by $c$ yields the same for $c t^{2}$. The identity map at $0$, scaled by $b$, gives derivative $b$ for $b t$. Adding those two maps and then the constant $a$ produces derivative $b$ for the sum form $c t^{2} + b t + a$. A funext/ring equality rewrites the target polynomial into that sum form; simpa finishes.
why it matters
The sole consumer is hasDerivAt_exactMidpointBlochSymbol_line, which asserts that $t \mapsto$ exactMidpointBlochSymbol$(H + t \cdot K, k)$ has derivative equal to the exact midpoint Bloch first variation at $t = 0$. That parent theorem is the finite-line directional derivative step inside the TT first-variation pipeline for the closed 4D midpoint Bloch continuum face.
Per the module header, the larger program transports this variation through the banked continuum limit S_RS_converges_EH_4d_closed on $H\pm K$ plus polarization. The lemma itself is pure calculus scaffolding: it does not touch the Recognition Composition Law, the forcing chain T0–T8, or any sourced Einstein response. It simply clears the elementary differentiability obligation so the cross-term first variation can be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.