hasDerivAt_numForm_zeroDot
plain-language theorem explainer
At a point where the numerator vanishes and the product of the two squared-norm factors equals 32, the derivative of the cleared-denominator cosine form N/(2√(PQ)) collapses to N'/(8√2). Analysts of the type-(1,2) Regge star kernel cite this when differentiating near and far apex-dot slots along coordinate paths. The proof is a quotient-rule calculation that plugs the two numerical gates into Mathlib's HasDerivAt chain.
Claim. Let $N,P,Q:\mathbb{R}\to\mathbb{R}$ be differentiable at $t_0$ with derivatives $N',P',Q'$. If $N(t_0)=0$ and $P(t_0)Q(t_0)=32$, then $\frac{d}{dt}\big|_{t_0}\frac{N(t)}{2\sqrt{P(t)Q(t)}}=\frac{N'}{8\sqrt{2}}$.
background
In the Regge 4D full periodic-lattice star deficit class kernel of type (1,2), dihedral cosines are read from Gram data via a cleared-denominator form. The numerator is an apex-dot product; the denominator is twice the geometric mean of two squared apex norms, matching the committed cosDihedral pattern from the Freudenthal incidence layer and the Gram-projection calculus.
The module enumerates the four (cube translate, Kuhn simplex) pairs that contain the representative hinge ${0,e_0,e_0+e_1+e_2}$, shows that all four simplices have flat cosine 0, and builds the full-star deficit class kernel on the 15 stencil classes with values $\pm\sqrt{2}/2$. Differentiating that cosine form along near and far coordinate paths needs a specialized derivative identity exactly at the flat point, where the numerator is zero and the product of squared norms is fixed at 32 by the lattice geometry.
proof idea
Product-rule the map $t\mapsto P(t)Q(t)$, then take the square-root derivative (legal because $PQ(t_0)=32\neq 0$), then scale by the constant 2 to obtain the denominator derivative. Form the quotient derivative of $N$ over that denominator. From $PQ(t_0)=32$ rewrite $\sqrt{PQ(t_0)}=4\sqrt{2}$. Convert the quotient-rule expression at the evaluation point: with $N(t_0)=0$ the cross term drops, and after field simplification and ring the claimed value $N'/(8\sqrt{2})$ remains.
why it matters
The private near-slot and far-slot derivative lemmas invoke this identity to obtain HasDerivAt for each of the ten stencil directions along the near and far coordinate paths. Those slot derivatives underwrite the full-star deficit class kernel gates listed in the module header: nonvacuity, swap-$1\leftrightarrow 2$ hinge-fixing symmetry, the uniform-scaling decoy $\sqrt{2}/2$, and homothety stationarity 0.
In the QG full-theory campaign this is the next kernel-checked increment after the type-(1,1) seed orbit. It does not close the flat Hessian over all hinges, does not prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, and does not flip gap_action_recovery. The complement-related type-(2,1) orbit remains open and is not transported here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.