t13_path4_polys
plain-language theorem explainer
When the type-(1,3) flat squared-edge configuration is deformed by replacing edge slot 4 with a real parameter t, the four cleared-denominator Gram quantities (apex-dot numerator, two apex norm-square numerators, hinge Gram determinant) become explicit quadratic polynomials in t. Anyone computing the slot-4 dihedral-cosine derivative at flatness cites this identity. The proof is pure algebraic expansion: unfold the four polynomial definitions and ring-normalize.
Claim. For every real $t$, if the ten squared edge lengths equal the flat type-$(1,3)$ values except that slot $4$ equals $t$, then the apex-dot numerator is $-4t^{2}+20t-16$, the third-apex norm-square numerator is $-2t^{2}+12t-10$, the fourth-apex norm-square numerator is $-3t^{2}+18t-19$, and the hinge Gram determinant is $-t^{2}+10t-9$.
background
The module builds the Regge 4D type-(1,3) periodic-lattice star deficit class kernel. After reordering so the triangle hinge occupies slots $(0,1,2)$ and the two apexes follow Freudenthal chain order, the flat local squared lengths are the fixed 10-tuple $t_{13}$ with values $(1,4,2,3,3,1,2,2,1,1)$. The one-parameter path $t\mapsto t_{13}[4\leftarrow t]$ freezes every slot except slot 4.
The four quantities are the cleared-denominator Gram numerators from the dihedral kernel: hinge Gram determinant $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^{2}$ (four times the squared hinge-area factor), the numerator of $\langle c',d'\rangle\cdot\mathrm{hingeGramDet}$ (apex projections orthogonal to the hinge plane), and the two numerators of $|c'|^{2}\cdot\mathrm{hingeGramDet}$ and $|d'|^{2}\cdot\mathrm{hingeGramDet}$. These feed the cosine of the dihedral angle via the Gram-projection calculus.
proof idea
Term-mode proof. Introduce the real parameter $t$, then split the four-way conjunction with refine. Each conjunct is discharged by the same two-step tactic block: simp unfolds apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet, the coordinate path (which substitutes $t$ only in slot 4), and the flat edge table; ring normalizes the resulting multivariate polynomial identity over $\mathbb{R}$. No external lemmas beyond the four definitions and the path/flat table are required.
why it matters
This identity is the algebraic fuel for hasDerivAt_t13_slot4, which obtains
$\mathrm{HasDerivAt},(\cos\mathrm{Dihedral}\circ t_{13}[4\leftarrow\cdot]),(-1/4),3$
by feeding the twelve polynomial coefficients into the cleared-denominator master derivative lemma at the flat point. That derivative is one of the ten coordinate derivatives demanded by deliverable A of the type-(1,3) star kernel (item 4 in the module brief). Together with the flat cosine multiset $1/2$ and the $2\pi$ angle-sum gate, the derivatives assemble the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$ with values $(\pm\sqrt{3})$. The complementary type-$(3,1)$ transport remains open; this lemma does not address it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.