path3_polys
plain-language theorem explainer
Along the path that varies only squared-edge slot 3 about the flat Freudenthal seed, the four Gram-projection numerators collapse to the explicit quadratics 8, 4, −t²+8t−8, and 4. The slot-3 HasDerivAt theorem for the dihedral cosine cites this identity to feed the generic quotient derivative machine. Proof is pure expansion: unfold the four polynomial defs on the path and ring-normalize.
Claim. For every real $t$, let $a(t)$ be the local squared-edge vector that equals $t$ in slot 3 and equals the flat seed values in the other nine slots. Then the cleared-denominator apex inner-product numerator is $8$, the first apex-norm-squared numerator is $4$, the second is $-t^2+8t-8$, and the hinge Gram determinant is $4$.
background
This module computes the seed-hinge dihedral cosine of a 4D Regge triangulation as an explicit algebraic function of the ten local squared edge lengths, then differentiates that cosine at the flat Freudenthal point. The cosine is realized in cleared-denominator Gram form: project the two apex vectors orthogonal to the hinge plane and take their normalized inner product.
The four building blocks are polynomial in the edge squares. hingeGramDet is $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^2$ for the two hinge edge-vectors from vertex 0. apexDotNum, apex3NormSqNum, and apex4NormSqNum are the numerators of $\langle c',d'\rangle$, $|c'|^2$, and $|d'|^2$ each multiplied by that Gram factor. The one-parameter path coordPath 3 t freezes nine edges at the flat seed and sets slot 3 equal to the real parameter $t$.
Every slot restriction of the cosine is then a quotient $N(t)/(2\sqrt{P(t)Q(t)})$; the present lemma records the four numerator polynomials on slot 3 so the generic derivative lemma can fire.
proof idea
Term-mode proof. Introduce $t$, split the four conjuncts with refine, then on each goal simp unfolds apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet, and coordPath (so slot 3 becomes $t$ and the other slots become the numeric flat seed). Finish each goal by ring, which normalizes the resulting multivariate polynomial identity over $\mathbb{R}$. No external lemmas beyond definitional unfolding.
why it matters
This is one of the ten slot-polynomial certificates that discharge deliverable A of the module: all ten coordinate derivatives of cosDihedral at the flat seed. Downstream, hasDerivAt_cosDihedral_slot3 feeds these coefficients (constant $N\equiv 8$, $P\equiv 4$, $Q=-t^2+8t-8$, $D\equiv 4$) into the generic hasDerivAt_slot machine and concludes that the slot-3 derivative of the cosine is $0$ at the flat value $t=4$.
Slots 0–7 are expected to give vanishing kernels; slot 3 is one of those bulk edges. The nonzero kernels live on slots 8 and 9 and assemble, after the arccos chain rule, into the two-simplex partial deficit gradient supported on edge classes $(3,7,11)$. The lemma is local scaffolding inside that kernel pipeline. It does not touch the still-open 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.