hasDerivAt_quadPoly
plain-language theorem explainer
The real quadratic polynomial at^{2} + bt + c is differentiable at every t₀ with derivative 2a t₀ + b. Gravity analysts cite it as the elementary engine under every cleared-denominator slot derivative of Regge dihedral cosines. The proof is pure calculus: power rule, constant scaling, and sum/const rules, finished by a ring identity.
Claim. For all real coefficients $a,b,c$ and every point $t_0\in\mathbb{R}$, the map $t\mapsto a t^2 + b t + c$ has derivative $2 a t_0 + b$ at $t_0$.
background
In the type-(1,3) Regge hinge kernel, every one-parameter restriction of a dihedral cosine along a squared-edge coordinate path is of the form $N(t)/(2\sqrt{P(t)Q(t)})$, where $N,P,Q$ are real quadratics. At the flat seed the cleared values are $(N,P,Q)=(8,8,8)$ (or the dihedral-kernel variant $(8,4,8)$). Differentiating the cosine therefore reduces to differentiating those three quadratics and assembling the quotient rule.
This private lemma supplies exactly that quadratic derivative. The surrounding module enumerates the six Kuhn simplices of the Freudenthal star on the hinge with absolute masks ${0,1,15}$, proves the flat cosine multiset is constantly $1/2$, and gates the angle sum to $2\pi$. The same quadratic derivative is duplicated across the sibling star-kernel modules so each file stays self-contained.
proof idea
Four short have steps. First, hasDerivAt_pow 2 t0 gives the derivative of $t\mapsto t^2$ as $2t_0$. Scale by the constant $a$ via const_mul. Independently, scale the identity map by $b$ to obtain the linear term. Add the two derivatives and then add the constant $c$ with add_const. A final convert ... using 1; ring rewrites the assembled derivative into the target expression $2a t_0 + b$.
why it matters
Item 4 of the module deliverable requires all ten coordinate derivatives of the star deficit via the cleared-denominator master lemma at flat $(N,P,Q)=(8,8,8)$. This lemma is the shared algebraic atom: every hasDerivAt_slot, hasDerivAt_opp_slot, hasDerivAt_orth_slot, hasDerivAt_near_slot and hasDerivAt_far_slot in the type-(1,3) and sibling kernels invokes it three times (once each for $N,P,Q$). Without it the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$ with values $(\pm\sqrt{3})$ cannot be differentiated. It does not itself close the open transport to the complementary type-(3,1) orbit, nor the flat Hessian assembly, nor $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.