opp_path2_polys
plain-language theorem explainer
Along the opposite-orbit edge path that varies squared length slot 2, the four dihedral Gram numerators are explicit quadratic polynomials in the path parameter t. Anyone differentiating the opposite-orbit dihedral cosine at the flat point cites this identity. The proof is a pure algebraic expansion: unfold the path and the four numerator defs, then ring.
Claim. For every real $t$, if one starts from the opposite-orbit flat squared-edge vector and replaces the slot-$2$ entry by $t$, then the hinge Gram determinant equals $4$, the apex-dot numerator equals $4t$, the third-apex squared-norm numerator equals $-t^2+8t-4$, and the fourth-apex squared-norm numerator equals $4$.
background
This module is the next kernel-checked increment in 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 dihedral cosine calculus from the two-simplex kernel and never redefines that API.
The four scalar functions here are the cleared-denominator ingredients of the dihedral cosine. 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 projections of the two free apexes orthogonal to the hinge plane, each multiplied by that Gram factor.
The opposite flat squared-edge vector is the fixed 10-tuple of squared lengths on one star orbit at the flat embedding. The opposite coordinate path of index $k$ freezes every slot except $k$, which is set to the real parameter $t$. Slot 2 is one of the free (non-hinge) edges on that orbit.
proof idea
Term-mode proof by introduction on $t$, then a four-way refine of the conjunction. Each conjunct is discharged by the same two-step tactic chain: simp unfolds apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet, the path definition, and the opposite flat edge table; ring finishes the polynomial identity. No external lemmas beyond definitional unfolding are required.
why it matters
This identity is the algebraic fuel for hasDerivAt_opp_slot2, which asserts that the opposite-orbit dihedral cosine, restricted to the slot-2 path, is differentiable at the flat value $t=2$ with derivative $\sqrt{2}/8$. That derivative gate sits inside the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$, and feeds the nonvacuity, swap-symmetry, and homothety-stationarity checks listed in the module deliverable.
In the broader QG campaign the lemma is pure scaffolding for the flat Hessian of the Regge action on this hinge orbit. It does not yet assemble the Hessian over all hinge orbits, nor does it touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence or gap-action recovery. Those remain explicitly open in the module tier tags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.