opp_path3_polys
plain-language theorem explainer
Along the opposite-orbit edge path that varies squared length slot 3, the four dihedral-cosine numerator polynomials collapse to explicit quadratics in the path parameter t. Anyone assembling the flat Hessian or stationarity gates for the seed hinge star cites this identity. The proof is a pure algebraic simplification: unfold the Gram numerators and ring-normalize.
Claim. For every real $t$, if the squared-edge 10-tuple equals the opposite-orbit flat configuration except that coordinate $3$ is set to $t$, then the apex-dot numerator equals $4t+4$, the third-apex norm-squared numerator equals $8$, the fourth-apex norm-squared numerator equals $-t^2+6t-1$, and the hinge Gram determinant equals $4$.
background
This 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, six incident 4-simplices. It sits one kernel increment past the two-simplex dihedral cosine calculus and never redefines that API.
The dihedral cosine of a 4-simplex about a triangular hinge is assembled from four real polynomials on the ten squared edge lengths: 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). The opposite-orbit flat configuration fixes those ten lengths to the integer multiset $(1,2,2,1,1,3,2,4,3,1)$. The coordinate path oppCoordPath 3 freezes every slot except index 3 and replaces that slot by a free real parameter $t$.
proof idea
Introduce the path parameter $t$. Split the four conjuncts with refine, then for each goal unfold the four numerator definitions together with the path and the opposite flat edge table, and finish by ring. No external lemmas beyond definitional unfolding are required; the identities are pure polynomial arithmetic on the ten edge slots.
why it matters
The identity supplies the exact coefficient list that hasDerivAt_opp_slot3 feeds into the generic one-slot derivative lemma for the opposite orbit. That derivative theorem shows the dihedral cosine is stationary (derivative zero) at the flat point $t=1$ when only slot 3 is varied. Stationarity of the cosine along each edge direction is a gate in the full-star deficit class kernel (classes $(2,3,6,7,10,11,14)$ with signs $(-1,-1,+1,-1,+1,+1,-1)$) and supports the homothety-stationarity and flatness checks listed in the module deliverable. It does not yet assemble the global flat Hessian or close the Einstein–Hilbert recovery gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.