opp_path1_polys
plain-language theorem explainer
Along the opposite-orbit edge path that varies squared length slot 1 about the flat configuration, the four dihedral-cosine numerators (apex dot product, two apex norms, hinge Gram determinant) collapse to explicit quadratic polynomials in the path parameter. Anyone checking stationarity of the opposite-class dihedral cosine cites this identity. The proof is a pure algebraic simplification: unfold the path and numerator definitions, then ring.
Claim. For every real $t$, if one deforms the opposite-orbit flat squared-edge vector by setting slot $1$ equal to $t$ and leaving all other slots fixed, then the apex-dot numerator equals $-4t^2+16t-8$, the third-apex norm-squared numerator equals $-3t^2+12t-4$, the fourth-apex norm-squared numerator equals $-2t^2+8t-4$, and the hinge Gram determinant equals $-t^2+4t$.
background
The module builds the full periodic Freudenthal star of the seed triangle hinge ${0,e_0,e_0+e_1}$ in the 4D integer lattice: four unit cubes and six incident 4-simplices. It never redefines the seed two-simplex dihedral calculus; it only evaluates that calculus on star members.
Squared edge lengths of a 4-simplex are packaged as a 10-slot vector. The opposite-orbit flat vector fixes those slots to the Euclidean values $(1,2,2,1,1,3,2,4,3,1)$. The opposite coordinate path replaces a single chosen slot by a real parameter $t$ while freezing the rest at those flat values.
The four scalar kernels come from the dihedral kernel: the hinge Gram determinant $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^2$, and the three numerators of the apex projections orthogonal to the hinge plane (dot product and two squared norms, each already multiplied by the Gram factor). Their ratios determine the dihedral cosine.
proof idea
Term-mode proof by direct expansion. Introduce the real parameter $t$, split into the four conjuncts, and on each goal unfold the four numerator definitions together with the opposite coordinate path and the opposite flat edge vector. After substitution every expression is a polynomial identity in $t$; ring closes all four goals.
why it matters
This identity is the algebraic fuel for hasDerivAt_opp_slot1, which proves that the opposite-orbit dihedral cosine is stationary (derivative zero) at the flat value $t=2$ when slot 1 is varied. That stationarity gate is one of the deliverable-A checks of the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$.
In the broader QG campaign the lemma sits one kernel increment past the two-simplex dihedral calculus: it supplies the explicit polynomials needed before any Hessian or continuum limit is assembled. It does not yet touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence or gap-action recovery; those remain open module-level goals. The calculation is lattice-orbit specific (opposite class only) and feeds the homothety-stationarity and flatness-gate story for the seed hinge star.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.