hasDerivAt_quadPoly
plain-language theorem explainer
The real quadratic polynomial at² + bt + c is differentiable everywhere, with derivative 2at₀ + b at any point t₀. Analysts of the Regge 4D star deficit cite it as the base calculus step for one-parameter edge deformations about the flat lattice. The proof chains Mathlib power and identity derivatives with constant-multiplication and addition rules, then closes by ring.
Claim. For all real coefficients $a,b,c$ and every real point $t_0$, the map $t \mapsto a t^2 + b t + c$ has derivative $2 a t_0 + b$ at $t_0$.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the two-simplex dihedral cosine calculus. It treats the seed triangle hinge and its full periodic Freudenthal star in the integer lattice: four containing unit cubes and six incident 4-simplices. Deliverables include star enumeration, the flat cosine multiset, the flatness gate (angle sum exactly $2\pi$), and the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$.
Dihedral cosines along one-parameter edge paths are rational functions $N(t)/(2\sqrt{P(t)\cdot Q(t)})$ whose numerator and denominator factors are quadratic polynomials in the deformed squared edge length. Differentiating those cosines at the flat point therefore reduces to ordinary real calculus on quadratics. The same private lemma is duplicated across the dihedral kernel and the star-kernel orbit files so each file stays self-contained.
proof idea
Standard Mathlib calculus assembly. First obtain HasDerivAt for $t\mapsto t^2$ via hasDerivAt_pow 2. Scale by the leading coefficient $a$ with const_mul. Independently differentiate the linear term $b t$ from hasDerivAt_id scaled by $b$. Add the two derivatives and the constant $c$ via add and add_const. A final convert plus ring matches the target derivative expression $2 a t_0 + b$.
why it matters
Without a certified derivative of the quadratic building blocks, none of the slot-wise stationarity lemmas for the star can fire. Downstream consumers include hasDerivAt_opp_slot and hasDerivAt_orth_slot in this module, the corresponding near/far slot derivatives in the 12-orbit kernel, and the generic hasDerivAt_slot path in the dihedral kernel. Those lemmas feed the homothety-stationarity and uniform-scaling decoy gates listed in the module deliverable list.
The lemma itself is pure real analysis; its place in Recognition Science is infrastructural. It supports the kernel-checked path toward flat Hessian assembly on the seed hinge orbit, while the module doc explicitly leaves open other hinge orbits, full Hessian assembly, $S_{RS}$ convergence to Einstein–Hilbert in 4D, and the gap-action recovery flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.