opp_path4_polys
plain-language theorem explainer
Along the opposite-orbit flat edge configuration, varying squared-edge slot 4 produces four explicit quadratics for the dihedral Gram numerators (apex dot, two apex norms, hinge Gram det). Cited by anyone checking first-order stationarity of the star dihedral cosine. Proof is pure simplification of the four numerator defs followed by ring.
Claim. For every real $t$, replace squared-edge coordinate $4$ of the opposite-orbit flat configuration by $t$. Then the apex-dot numerator equals $-2t^2+12t-2$, the third-apex norm-squared numerator equals the same quadratic, and both the fourth-apex norm-squared numerator and the hinge Gram determinant equal $-t^2+6t-1$.
background
Module is the Regge 4D full periodic-lattice star deficit class kernel: seed hinge ${0,e_0,e_0+e_1}$ and its six-simplex Freudenthal star in the integer lattice. It imports the two-simplex dihedral cosine calculus and never redefines that API.
The four quantities are rational numerators from the dihedral kernel. hingeGramDet is $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^2$ on the hinge edge-vectors (four times the squared hinge-area factor). apexDotNum, apex3NormSqNum, apex4NormSqNum are the numerators of $\langle c',d'\rangle$, $|c'|^2$, $|d'|^2$ times that determinant, with $c',d'$ the apex projections orthogonal to the hinge plane.
oppFlatSqEdges is the squared-edge 10-vector of the opposite flat orbit. oppCoordPath k t freezes every slot except $k$, which is set to the real parameter $t$. Here $k=4$.
proof idea
Term-mode proof. Introduce $t$, split the four conjuncts with refine, then on each goal simp unfolds apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet, oppCoordPath, and oppFlatSqEdges. The resulting polynomial identities are discharged by ring. No external lemmas beyond those definitions.
why it matters
Feeds hasDerivAt_opp_slot4, which shows the dihedral cosine along this path has derivative $0$ at the flat point $t=1$. That stationarity gate is one of the deliverables of the full-star deficit class kernel (classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$), together with nonvacuity, swap symmetry, and the uniform-scaling decoy.
In the QG campaign this is the next kernel-checked increment after the seed dihedral cosine calculus. It does not yet assemble the flat Hessian over all hinges, nor prove $S_{RS}$ converges to Einstein–Hilbert in 4D, nor flip gap_action_recovery. It is local algebraic fuel for the homothety-stationarity check on one opposite-orbit slot.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.