opp_path6_polys
plain-language theorem explainer
Along the path that varies only the sixth squared edge of an opposite-orbit flat 4-simplex, the hinge Gram determinant and the three apex-projection numerators collapse to explicit quadratics in the path parameter. Star-deficit Hessian work cites this to feed the dihedral-cosine derivative at the flat point. Proof is unfold-and-ring on the four polynomial definitions.
Claim. For every real $t$, replace the sixth squared edge length of the opposite-orbit flat edge vector by $t$ (other nine entries fixed). Then the hinge Gram determinant equals $4$, the apex-dot numerator equals $8$, the third-apex norm-squared numerator equals $8$, and the fourth-apex norm-squared numerator equals $-2t^{2}+8t-4$.
background
Module is the Regge 4D full periodic-lattice star deficit class kernel: seed triangle hinge and its six incident 4-simplices in the integer Freudenthal lattice. It imports the dihedral cosine calculus (Gram numerators) and never redefines that API.
The four quantities are 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 scaled by the Gram determinant). They are the algebraic ingredients of the dihedral cosine of a 4-simplex about the seed hinge.
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 nine slots at those flat values and substitutes the real parameter $t$ into slot 6. This lemma records the resulting four polynomials.
proof idea
Term-mode proof: introduce $t$, split the four conjuncts with refine, then on each goal simp unfolds the four numerator definitions together with the coordinate path and the opposite flat edge vector, after which ring normalizes the resulting polynomial identity. No external lemmas beyond definitional unfolding.
why it matters
Feeds hasDerivAt_opp_slot6, which asserts that the dihedral cosine along this path has derivative zero at the flat value $t=2$. That derivative gate is part of deliverable A of the star kernel: full-star deficit class values on classes $(2,3,6,7,10,11,14)$ and the homothety-stationarity and uniform-scaling decoy gates.
In the QG campaign this is one slot of the opposite-orbit path family needed before any flat Hessian assembly over the star. It does not touch the open hinge orbits, nor $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, nor gap-action recovery. Landmark context is classical Regge calculus on the lattice star, not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.