hasDerivAt_numForm_t13
plain-language theorem explainer
At the flat point where the Gram numerator and both squared-norm factors equal 8, the map t ↦ N(t)/(2√(P(t)Q(t))) has derivative (2N'−P'−Q')/32. Type-(1,3) Regge star analysts cite it as the shared cleared-denominator master identity for all ten coordinate slots. The proof chains product, square-root, and quotient rules, then collapses algebraically at the flat 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)=P(t_0)=Q(t_0)=8$, then $$\frac{d}{dt}\Big|_{t_0}\frac{N(t)}{2\sqrt{P(t)\,Q(t)}}=\frac{2N'-P'-Q'}{32}.$$
background
In the Regge 4D type-(1,3) periodic-lattice star deficit kernel, the cosine of a dihedral angle is written via a Gram-projection formula of the shape $N/(2\sqrt{PQ})$, where $N$ is an apex-dot numerator and $P,Q$ are squared-norm numerators on the two faces meeting the hinge. At the flat lattice configuration these three cleared-denominator polynomials evaluate to $(8,8,8)$, giving cosine $1/2$ and dihedral angle $\pi/3$.
The module enumerates the six Kuhn simplices of the Freudenthal star that contain the type-(1,3) hinge (absolute masks ${0,1,15}$), proves the flat angle sum is exactly $2\pi$, and differentiates the cosine expression along each of the ten coordinate deformation paths. This lemma is the shared analytic engine for those ten derivatives: it runs the chain rule once at the universal flat point rather than repeating the algebra per slot.
proof idea
Form the product $P\cdot Q$ by the product rule, then differentiate $\sqrt{PQ}$ (using $PQ(t_0)=64\neq 0$), then scale by the constant 2 to obtain the denominator derivative. Apply the quotient rule to $N$ over that denominator. Convert the resulting symbolic derivative by substituting the flat values $N=P=Q=8$ and $\sqrt{PQ}=8$, and finish with a ring simplification that collapses the expression to $(2N'-P'-Q')/32$.
why it matters
Deliverable A of the type-(1,3) star kernel requires all ten coordinate derivatives of the cosine form at flat. This master lemma is the single algebraic reduction those slots share; its immediate consumer is the per-slot specialisation that feeds each quadratic path $t\mapsto$ (apex-dot num, apex-3 norm-sq num, apex-4 norm-sq num) along the ten edge-coordinate deformations.
Together with the flat cosine multiset (all six simplices have cosine $1/2$) and the flatness gate (star angle sum $2\pi$), the derivatives feed the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$ with values $(\pm\sqrt{3})$. The module does not yet complete the flat Hessian over all hinges, prove $S_{RS}$ converges to Einstein–Hilbert in 4D, or flip gap-action recovery; transport of this kernel to the complementary type $(3,1)$ remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.