far_path9_polys
plain-language theorem explainer
Along the far-orbit path that varies only squared-edge slot 9, the four cleared-denominator Gram numerators are the explicit quadratics 0·t²−8t+24, 8, 4, and 8. Anyone differentiating the far dihedral cosine at the flat point cites this identity. The proof unfolds the path and numerator definitions, then finishes by ring.
Claim. For every real $t$, let $a(t)$ be the squared-edge 10-tuple equal to the far flat configuration except that coordinate $9$ equals $t$. Then the apex-dot numerator of $a(t)$ is $-8t+24$, the third-apex norm-squared numerator is $8$, the fourth-apex norm-squared numerator is $4$, and the hinge Gram determinant is $8$.
background
Module scope is the type-(1,2) triangle hinge in the 4D Freudenthal lattice and its full periodic star (two unit cubes, four incident 4-simplices). The campaign builds a full-star deficit class kernel on the 15 stencil classes; this lemma is a local algebraic step inside the far-orbit cosine calculus.
Squared edges live in a 10-slot vector SqEdges4. The far flat background is the fixed tuple $(1,3,1,2,2,2,1,4,1,3)$. The path farCoordPath 9 t replaces only slot 9 by the free real parameter $t$.
The four scalar functions are the cleared-denominator Gram pieces from the dihedral kernel: hinge Gram determinant $4a_0 a_1-(a_0+a_1-a_4)^2$; apex-dot numerator of $\langle c',d'\rangle\cdot\mathrm{hingeGramDet}$; and the two apex norm-squared numerators of $|c'|^2$ and $|d'|^2$ times that determinant. They feed the committed cosDihedral formula.
proof idea
Term-mode proof after intro t. Split the four conjuncts with refine, then on each goal simp unfolds apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet, farCoordPath, and farFlatSqEdges. The resulting polynomial identities are discharged by ring. No external lemmas beyond definitional unfolding.
why it matters
Supplies the exact coefficient tuple needed by hasDerivAt_far_slot9, which asserts
$\mathrm{HasDerivAt},(\cos\mathrm{Dihedral}\circ\mathrm{farCoordPath},9),((-8)/(8\sqrt{2})),3$.
That derivative is one slot of the far-orbit linearization used to assemble the type-(1,2) full-star deficit class kernel (deliverable A of the module: flat cosine multiset, flatness gate $4\cdot\arccos 0=2\pi$, and stencil values $\pm\sqrt{2}/2$).
The module sits in the QG full-theory campaign after the type-(1,1) seed orbit. It does not close the complementary type-(2,1) orbit, the global flat Hessian, or S_RS_converges_EH_4d. Within those limits, this polynomial gate is the concrete algebraic input that lets the far-slot-9 derivative fire without numeric decision procedures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.