hasDerivAt_numForm
plain-language theorem explainer
At the flat point where the Gram numerator is 8 and the two projected-norm squares are 4 and 8, the map t ↦ N(t)/(2√(P(t)Q(t))) is differentiable with derivative √2(2N'−2P'−Q')/32. Cited when differentiating the seed-hinge dihedral cosine along squared-edge paths. Proof is standard quotient/product/sqrt calculus followed by algebraic reduction at those three values.
Claim. Let $N,P,Q:\mathbb{R}\to\mathbb{R}$ be differentiable at $t_0$ with derivatives $N',P',Q'$. If $N(t_0)=8$, $P(t_0)=4$, and $Q(t_0)=8$, then $\frac{d}{dt}\big|_{t_0}\frac{N(t)}{2\sqrt{P(t)Q(t)}}=\frac{\sqrt{2}\,(2N'-2P'-Q')}{32}$.
background
The module treats the seed-triangle hinge ${0,e_0,e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices in the 4D Regge lattice. Deliverable A is the Gram-projection cosine of the dihedral angle as an explicit function of the ten local squared edge lengths: numerator from the projected apex inner product, denominator twice the product of projected apex norms (cleared-denominator form).
At the flat Freudenthal point one has $\cos=1/\sqrt{2}$. The three scalar functions $N,P,Q$ stand for that numerator and the two squared-norm factors along a real path in edge-length space. Their flat values $N=8$, $P=4$, $Q=8$ are the arithmetic input to this lemma; they make $\sqrt{PQ}=4\sqrt{2}$ and the denominator $8\sqrt{2}$.
The lemma is pure real calculus (Mathlib HasDerivAt). Upstream depends_on edges into foundation/PRC modules are incidental identifier collisions on div/from, not conceptual inputs.
proof idea
Build the derivative of the composite bottom-up. First hP.mul hQ gives the product rule for $PQ$, then HasDerivAt.sqrt (using $PQ(t_0)=32\neq 0$) and a constant factor 2 give the denominator derivative. Quotient rule via hN.div yields a raw derivative expression.
convert aligns that expression with the target. The remaining algebra: rewrite $\sqrt{32}=4\sqrt{2}$, expand the squared denominator to 128, and apply the identity $X/(2\cdot 4\sqrt{2})=X\sqrt{2}/16$. A final ring collapses the numerator to $\sqrt{2}(2N'-2P'-Q')/32$.
why it matters
Private calculus engine for hasDerivAt_slot, which differentiates the Gram cosine along each of the ten coordinate paths (quadratic numerator/norm polynomials in the path parameter). That slot lemma packages the ten coordinate derivatives of cosDihedral at flat: slot 8 ↦ $\sqrt{2}/8$, slot 9 ↦ $-\sqrt{2}/4$, slots 0–7 ↦ 0, assembled as cosDihedralKernel under the master theorem hasDerivAt_cosDihedral_coord.
Those kernels feed the arccos chain factor $-1/\sin=-\sqrt{2}$ at flat, producing the local angle kernel and the two-simplex partial deficit gradient supported on edge classes $(3,7,11)$. In the QG campaign this is the next kernel-checked increment after ReggeHinge4DFlatKernel. It does not close the full lattice orbit sum, the flat Hessian of the 4D Regge action, or S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.