opp_path8_polys
plain-language theorem explainer
Along the opposite-orbit squared-edge path that varies only slot 8, the four Gram numerators (apex inner product, two apex norms, hinge Gram determinant) collapse to explicit quadratics in the path parameter. Anyone differentiating the dihedral cosine at the flat opposite configuration cites this identity. The proof is a direct simp-and-ring expansion of the polynomial definitions.
Claim. For every real $t$, let the squared-edge 10-vector equal the opposite-orbit flat configuration except that coordinate $8$ is set to $t$. Then the apex-dot numerator equals $8$, the third-apex norm-squared numerator equals $8$, the fourth-apex norm-squared numerator equals $-t^{2}+6t-5$, and the hinge Gram determinant equals $4$.
background
Module scope is the seed triangle hinge and its full periodic Freudenthal star in the integer lattice (four unit cubes, six incident 4-simplices). The campaign builds the full-star deficit class kernel after the two-simplex dihedral cosine calculus of ReggeHinge4DDihedralKernel.
The four scalar kernels are polynomial numerators in the ten squared edge lengths: 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$ that determinant; and the two apex norm-squared numerators of $|c'|^{2}$ and $|d'|^{2}$ times the same factor. The opposite-orbit flat squared-edge vector is the fixed 10-tuple $(1,2,2,1,1,3,2,4,3,1)$. The coordinate path freezes every slot except index $k$, replacing that entry by the real parameter $t$.
proof idea
Term-mode proof. Introduce $t$, then split the four conjuncts with refine. Each goal is discharged by simp unfolding the four numerator definitions together with the opposite coordinate path and the opposite flat edge vector, followed by ring to normalize the resulting polynomial in $t$. No external lemmas beyond those unfoldings.
why it matters
Supplies the exact quadratic coefficients that hasDerivAt_opp_slot8 feeds into the generic opposite-slot derivative lemma, proving that the dihedral cosine along this path has derivative zero at the flat value $t=3$. That stationarity gate is one of the deliverables of the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$. It sits inside the QG campaign that aims at flat Hessian assembly and eventual $S_{\mathrm{RS}}\to$ Einstein–Hilbert recovery, without yet closing those larger goals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.