t13_path3_polys
plain-language theorem explainer
Along the path that varies only squared-edge slot 3 of the flat type-(1,3) star configuration, the four Gram-projection numerators collapse to explicit quadratics in the path parameter. Anyone differentiating the dihedral cosine at the flat point cites this identity. The proof unfolds the four numerator definitions and the path, then closes each identity by ring normalization.
Claim. For every real $t$, let $a(t)$ be the ten squared-edge lengths equal to the flat type-$(1,3)$ star values except that coordinate $3$ equals $t$. Then the numerator of the apex inner product times the hinge Gram determinant is $8$, the numerator of the first apex squared norm times that determinant is $8$, the numerator of the second apex squared norm times that determinant is $-3t^2+18t-19$, and the hinge Gram determinant itself is $12$.
background
This module builds the Regge 4D type-(1,3) periodic-lattice star deficit class kernel. The hinge has absolute masks ${0,1,15}$ with local flat squared lengths $(1,3,4)$; the star is the full Freudenthal star of six Kuhn simplices in the origin cube. Flat cosine is $1/2$ on every member, so the angle sum is exactly $2\pi$.
The dihedral cosine is recovered from four cleared-denominator polynomials on the ten squared edges: the hinge Gram determinant $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^2$, and the three numerators of $\langle c',d'\rangle$, $|c'|^2$, and $|d'|^2$ each multiplied by that determinant (apex projections orthogonal to the hinge plane). The flat configuration is the fixed 10-tuple with values $(1,4,2,3,3,1,2,2,1,1)$ after hinge-first reordering.
The coordinate path freezes every slot at those flat values and replaces a single slot $k$ by a real parameter $t$. Slot $3$ is one of the ten edges whose first derivative of cosine must be shown to vanish at the flat point.
proof idea
Term-mode proof. Introduce the real parameter $t$, then split the four conjuncts with refine. On each goal, simp unfolds the four numerator definitions together with the coordinate path and the flat squared-edge table, substituting $t$ only in slot $3$. Each resulting polynomial identity is closed by ring. No external lemmas beyond the definitions are required.
why it matters
This identity is the polynomial witness fed to the master cleared-denominator derivative lemma for slot 3. Downstream, hasDerivAt_t13_slot3 applies that master lemma at the flat values $(N,P,Q)=(8,8,8)$ with the coefficients recorded here, concluding that the derivative of dihedral cosine along the slot-3 path vanishes at the flat point $t=3$.
It is one of the ten coordinate-derivative legs that assemble the full-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})$. The module is the next kernel-checked increment after the type-$(1,1)$ seed orbit; transport of the kernel to the complementary type $(3,1)$ remains open, and the result does not yet complete flat Hessian assembly or flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.