t13_path0_polys
plain-language theorem explainer
Along the type-(1,3) flat squared-edge path that varies only slot 0, the four Gram numerators (apex dot, two apex norms, hinge Gram det) collapse to explicit quadratics in the path parameter. Cited by anyone building the cleared-denominator dihedral cosine derivative at the flat point. Proof is unfold-and-ring after substituting the path into the four numerator definitions.
Claim. For every real $t$, replace squared-edge slot $0$ of the type-$(1,3)$ flat configuration by $t$ and keep the other nine slots fixed. Then the apex-dot numerator equals $-2t^{2}+12t-2$, the first apex norm-squared numerator equals $-2t^{2}+12t-2$, the second equals $-t^{2}+10t-1$, and the hinge Gram determinant equals $-t^{2}+14t-1$.
background
Module is the Regge 4D type-(1,3) periodic-lattice star deficit kernel: the triangle hinge with absolute masks ${0,1,15}$ (local flat squared lengths $(1,3,4)$) and its full Freudenthal star. Deliverable A includes all ten coordinate derivatives of the dihedral cosine via a cleared-denominator master lemma at flat values $(N,P,Q)=(8,8,8)$.
The four polynomials come from the Gram-projection cosine calculus. hingeGramDet is $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^{2}$ for the hinge edge-vectors from vertex 0. apexDotNum, apex3NormSqNum, and apex4NormSqNum are the numerators of $\langle c',d'\rangle\cdot\mathrm{hingeGramDet}$ and $|c'|^{2}\cdot\mathrm{hingeGramDet}$, $|d'|^{2}\cdot\mathrm{hingeGramDet}$ for the apex projections orthogonal to the hinge plane.
t13FlatSqEdges is the flat local squared-edge 10-tuple after reordering so the hinge occupies slots $(0,1,2)$. t13CoordPath k t replaces only slot $k$ by the real parameter $t$.
proof idea
Term-mode proof. Introduce $t$, then split the four conjuncts with refine. Each goal is discharged by simp unfolding apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet, t13CoordPath, and t13FlatSqEdges, followed by ring to normalize the resulting polynomial identity. No external lemmas beyond the definitions.
why it matters
Feeds hasDerivAt_t13_slot0, which applies the master cleared-denominator derivative lemma at the flat point $t=1$ with these exact coefficient tuples and concludes that the derivative of the dihedral cosine along slot-0 is zero. That is one of the ten coordinate derivatives required for deliverable A of the type-(1,3) star kernel (flat cosine multiset $1/2$, star angle sum $2\pi$, full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$).
Sits inside the QG full-theory campaign after the type-(1,1) seed orbit and the orbit classification layer. Does not itself close Hessian assembly, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap-action recovery; those remain open per the module tier tags. Transport of this kernel to the complementary type $(3,1)$ is also still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.