hasDerivAt_numForm_opp
plain-language theorem explainer
At the flat point where the numerator equals 8 and the two Gram factors equal 8 and 4, the quotient N/(2√(P Q)) is differentiable with derivative √2(2N'−P'−2Q')/32. Used by the opposite-slot path derivative in the 4D Regge star kernel. Proof is the quotient rule plus constant arithmetic at those 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)=8$, and $Q(t_0)=4$, then $\frac{d}{dt}\big|_{t_0}\frac{N(t)}{2\sqrt{P(t)Q(t)}}=\frac{\sqrt{2}\,(2N'-P'-2Q')}{32}$.
background
The module builds the full periodic Freudenthal star deficit kernel for the seed triangle hinge in 4D Regge calculus: six incident 4-simplices across four unit cubes, with flat cosine multiset and angle sum $2\pi$. Opposite-orbit Gram data enter a cosine-style quotient whose numerator and two squared-norm factors are written $N$, $P$, $Q$.
At the flat evaluation point those factors take the concrete values $N=8$, $P=8$, $Q=4$, so $\sqrt{PQ}=4\sqrt{2}$ and the denominator is $8\sqrt{2}$. Differentiability of the quotient along a one-parameter path is needed before any stationarity or Hessian gate on the opposite slot can be stated.
The lemma is pure real calculus: it assumes only HasDerivAt for $N,P,Q$ at $t_0$ and the three constant evaluations; no lattice combinatorics appear in the statement.
proof idea
Form the product $PQ$ by the product rule, then differentiate $\sqrt{PQ}$ (nonzero at the flat point since $PQ=32$). Scale by 2 for the denominator. Apply the quotient rule to $N$ over that denominator.
convert reduces the goal to equality of the two derivative expressions. Substitute $N=8$, $P=8$, $Q=4$ and $\sqrt{PQ}=4\sqrt{2}$. Simplify the denominator derivative to $(P'+2Q')/\sqrt{2}$, clear denominators with field_simp, replace $(\sqrt{2})^2$ by 2, and finish by ring. The target coefficient $\sqrt{2}(2N'-P'-2Q')/32$ is exactly the reduced quotient-rule value.
why it matters
Immediate consumer is hasDerivAt_opp_slot, which differentiates the opposite-orbit cosine form along the ten coordinate paths of the star kernel. That slot derivative is part of the analytic package supporting the module's gates: nonvacuity, swap symmetry, uniform-scaling decoy, and homothety stationarity on the full-star deficit class kernel with values $(-1,-1,+1,-1,+1,+1,-1)$ on classes $(2,3,6,7,10,11,14)$.
In the QG campaign this is a kernel-checked increment after the dihedral cosine calculus: it does not assemble the flat Hessian over all hinges, does not prove $S_{RS}$ converges to Einstein–Hilbert in 4D, and does not flip gap-action recovery. It is local analytic plumbing so opposite-orbit first derivatives exist in closed form at the flat point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.