t13_path5_polys
plain-language theorem explainer
Along the type-(1,3) flat squared-edge path that varies only slot 5, the four cleared-denominator Gram quantities (apex-dot numerator, two apex-norm-squared numerators, hinge Gram determinant) equal explicit quadratics in the path parameter. Anyone building the ten flat coordinate derivatives of the dihedral cosine cites this identity. The proof substitutes the path into the four polynomial definitions and finishes by ring.
Claim. For every real $t$, let $a(t)$ be the squared-edge $10$-tuple equal to the type-$(1,3)$ flat configuration except that entry $5$ is $t$. Then the apex-dot numerator is $4t+4$, the first apex norm-squared numerator is $-4t^2+16t-4$, the second apex norm-squared numerator is the constant $8$, and the hinge Gram determinant is the constant $12$.
background
This module is the QG kernel for the type-$(1,3)$ triangle hinge on the 4D periodic Freudenthal lattice (absolute masks ${0,1,15}$, local flat squared lengths $(1,3,4)$). It enumerates the six-simplex star, checks flat angle sum $2\pi$, and supplies the full-star deficit class kernel; transport to the complementary type $(3,1)$ remains open.
The dihedral cosine is computed from Gram data on the two apexes projected orthogonal to the hinge plane. Four cleared-denominator polynomials package that data: hinge Gram determinant $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^2$; apex-dot numerator of $\langle c',d'\rangle\cdot\mathrm{hingeGramDet}$; and the two apex norm-squared numerators of $|c'|^2\cdot\mathrm{hingeGramDet}$ and $|d'|^2\cdot\mathrm{hingeGramDet}$.
The flat local squared edges (after reordering so the hinge occupies slots $(0,1,2)$) are the fixed $10$-tuple with values $(1,4,2,3,3,1,2,2,1,1)$. The coordinate path freezes every entry except slot $k$, replacing that entry by the real parameter $t$.
proof idea
Introduce the real parameter $t$. Split the four conjuncts with refine, then on each goal simp unfolds the four numerator definitions together with the coordinate path and the flat squared-edge table, after which ring normalizes the resulting polynomial identity in $t$. No external lemmas beyond those definitions are required.
why it matters
Deliverable A of the type-$(1,3)$ star kernel demands all ten coordinate derivatives of the dihedral cosine at the flat point, via the cleared-denominator master lemma evaluated at $(N,P,Q)=(8,8,8)$. This lemma supplies the exact quadratic coefficients for path slot $5$, which the parent theorem hasDerivAt_t13_slot5 feeds into that master lemma to obtain HasDerivAt (cosDihedral ∘ path_5) 0 1.
The resulting zero derivative is one of the ten flat directional derivatives that assemble the star deficit class kernel on classes $(1,3,5,7,9,11,13)$ with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$. It does not by itself close the flat Hessian over all hinges, nor the Einstein–Hilbert recovery gates flagged open in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.