opp_path0_polys
plain-language theorem explainer
Along the opposite-orbit edge path that varies only squared length slot 0, the four dihedral Gram numerators collapse to explicit quadratics in the path parameter t. Anyone checking flat-stationarity of the star dihedral cosine cites this identity. The proof is pure simplification: unfold the four numerator polynomials and the path, then ring-normalize.
Claim. For every real $t$, if the squared-edge 10-vector equals the opposite-orbit flat configuration except that coordinate $0$ is set to $t$, then the apex-dot numerator equals $-6t^2+20t-6$, the first apex-norm-squared numerator equals $-4t^2+16t-4$, the second apex-norm-squared numerator equals $-3t^2+10t-3$, and the hinge Gram determinant equals $-t^2+6t-1$.
background
This module is the next kernel-checked increment in the 4D Regge full-star campaign. It works on the seed triangle hinge ${0,e_0,e_0+e_1}$ and its full periodic Freudenthal star (four unit cubes, six incident 4-simplices). The deliverable is a deficit-class kernel on the star, not yet the global flat Hessian or Einstein–Hilbert recovery.
Squared edge data live in a 10-slot vector SqEdges4. The opposite-orbit flat configuration fixes those slots to concrete positive values (1,2,2,1,1,3,2,4,3,1). The coordinate path freezes every slot except index $k$, replacing slot $k$ by a real parameter $t$.
The four scalar polynomials come from the seed two-simplex dihedral calculus: 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 projected apex inner products and norms (each already multiplied by that determinant). Their ratios determine the dihedral cosine used downstream.
proof idea
Introduce the real parameter $t$. Split the four conjuncts with refine. On each goal, simp unfolds the four numerator definitions together with the opposite-orbit path and the fixed flat edge vector, substituting the concrete numeric slots. The resulting polynomial identities are discharged by ring. No external lemmas beyond those definitions are required.
why it matters
The identity supplies the exact coefficient list that hasDerivAt_opp_slot0 feeds into the generic one-slot derivative lemma for the opposite orbit. That parent theorem concludes that the dihedral cosine along this path has derivative zero at the flat point $t=1$, a stationarity gate for the full-star deficit class kernel.
In the module's deliverable list this supports the homothety-stationarity and flatness gates on classes $(2,3,6,7,10,11,14)$. It does not yet assemble the Hessian over all hinge orbits, nor does it touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or gap-action recovery. Within Recognition gravity it is a local algebraic checkpoint on the Regge side of the continuum limit, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.