opp_path5_polys
plain-language theorem explainer
Along the opposite-orbit edge path that varies only squared-length slot 5, the four Gram numerators (apex dot product, two apex norms, hinge Gram determinant) 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 direct simp-and-ring evaluation of the four polynomial definitions on the path.
Claim. For every real $t$, if one replaces squared-edge coordinate $5$ by $t$ in the opposite-orbit flat edge vector and leaves the other nine coordinates fixed, then the apex-dot numerator equals $8$, the first apex-norm numerator equals $-2t^2+12t-10$, the second apex-norm 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 after the two-simplex dihedral cosine calculus. Scope is the seed triangle hinge and its full periodic Freudenthal star (four unit cubes, six incident 4-simplices) in the integer lattice; other hinge orbits remain open.
The opposite-orbit flat squared-edge vector fixes ten edge lengths of a 4-simplex containing the hinge. The coordinate path at slot $k$ replaces only that squared length by a real parameter $t$. Four scalar polynomials built from those edges control the dihedral cosine: 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 multiplied by the Gram factor).
Slot 5 is one of the ten edge classes that must be differentiated when checking homothety stationarity and the flat Hessian contribution of the opposite orbit.
proof idea
Introduce the real parameter $t$. Split the four-way conjunction with refine, then for each conjunct unfold the four numerator definitions together with the path and the opposite flat edge vector, and finish by ring. No external lemmas are required beyond definitional expansion; the identities are pure polynomial arithmetic on the fixed flat coordinates with one free slot.
why it matters
The identity supplies the exact coefficient list consumed by hasDerivAt_opp_slot5, which proves that the dihedral cosine along this path has derivative zero at the flat value $t=3$. That derivative gate is part of deliverable A of the module: the full-star deficit class kernel and its stationarity checks (nonvacuity, swap symmetry, uniform-scaling decoy, homothety stationarity).
In the broader QG campaign this is a kernel brick toward assembling the flat Hessian on the seed hinge star. It does not yet close flat Hessian assembly over all hinges, nor S_RS_converges_EH_4d, nor gap_action_recovery. It sits strictly inside the Regge lattice analysis layer, not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.