opp_path7_polys
plain-language theorem explainer
Along the opposite-orbit path that frees squared edge slot 7 and holds the other nine edges at their flat values, the four Gram numerators (apex inner product, two apex squared norms, hinge Gram determinant) collapse to explicit quadratics in the free length. Anyone differentiating the dihedral cosine on this orbit cites these identities. The proof is a pure unfold-and-ring computation from the flat edge table.
Claim. For every real $t$, if the squared-edge $10$-tuple equals the opposite-orbit flat configuration except that coordinate $7$ is set to $t$, then the apex-dot numerator equals $8$, the third-apex norm-squared numerator equals $-t^{2}+8t-8$, the fourth-apex norm-squared numerator equals $4$, and the hinge Gram determinant equals $4$.
background
This module is the next kernel-checked increment of the 4D Regge full-star campaign: the seed triangle hinge and its full periodic Freudenthal star (four unit cubes, six incident 4-simplices). It imports the two-simplex dihedral cosine calculus and never redefines that API.
The four scalar functions are the numerators that enter the cosine of the dihedral angle at the hinge. The hinge Gram determinant is $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^{2}$ for the two hinge edge-vectors from vertex 0. The apex-dot and apex-norm numerators are the corresponding cleared-denominator expressions for the projections of the two free apexes orthogonal to the hinge plane.
The opposite-orbit flat squared-edge table fixes nine of the ten edge lengths of a 4-simplex; the coordinate path frees one slot (here slot 7) to a real parameter $t$ while leaving the rest at those flat values. Slot 7 is one of the seven deficit-class edges tracked by the full-star kernel.
proof idea
Introduce the free real parameter $t$. Split the four conjuncts with refine, then on each goal unfold the four numerator definitions together with the opposite-orbit coordinate path and the opposite flat edge table. After simplification the identities are polynomial equalities in $t$; close each by ring.
why it matters
The lemma is the polynomial certificate consumed by the opposite-orbit slot-7 derivative theorem, which shows that the dihedral cosine along this path has derivative zero at the flat point $t=4$. That stationarity gate is one of the five deliverables of the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$.
In the broader QG campaign this is incremental kernel work after the seed dihedral calculus: it supports the flatness gate (star angle sum $2\pi$) and the homothety-stationarity checks, without yet assembling the flat Hessian over all hinge orbits or claiming Einstein–Hilbert recovery. Other hinge orbits of the lattice remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.