far_path5_polys
plain-language theorem explainer
Along the far-orbit edge path that varies only squared length slot 5, the four cleared-denominator Gram quantities (apex inner product numerator, two apex-norm numerators, and hinge Gram determinant) are explicit quadratic polynomials in the path parameter t. Anyone differentiating the dihedral cosine along this path cites it. The proof is a direct expand-and-ring simplification of the four polynomial definitions on the path.
Claim. For every real $t$, if one takes the far-orbit squared-edge vector and replaces coordinate $5$ by $t$, then the apex-dot numerator equals $4t-8$, the first apex-norm-squared numerator equals $-3t^2+12t-4$, the second apex-norm-squared numerator equals the constant $4$, and the hinge Gram determinant equals the constant $8$.
background
This module is the type-$(1,2)$ full periodic-lattice star deficit kernel for 4D Regge calculus: the triangle hinge with masks ${0,1,7}$ and its four incident Kuhn 4-simplices in the Freudenthal triangulation. Dihedral cosines are computed from squared edge lengths via a committed cleared-denominator Gram calculus, never by floating-point or native_decide.
The four scalar functions here are the numerators that enter that calculus. hingeGramDet 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. apexDotNum, apex3NormSqNum, and apex4NormSqNum are the corresponding numerators of $\langle c',d'\rangle\cdot\mathrm{hingeGramDet}$ and $|c'|^2\cdot\mathrm{hingeGramDet}$, $|d'|^2\cdot\mathrm{hingeGramDet}$ for the two apex projections orthogonal to the hinge plane.
farFlatSqEdges is one of the two flat squared-length orbits on the star (values $1,3,1,2,2,2,1,4,1,3$ on slots $0..9$). farCoordPath k t freezes that orbit and replaces only slot $k$ by the real parameter $t$. Slot $5$ is one of the ten stencil classes whose one-parameter variation feeds the full-star deficit kernel.
proof idea
One-line algebraic verification. Introduce $t$, split the four conjuncts with refine, then simp unfolds apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet, farCoordPath, and farFlatSqEdges (so slot 5 becomes $t$ and every other slot is a concrete integer). Each goal reduces to a polynomial identity closed by ring.
why it matters
Feeds hasDerivAt_far_slot5, which asserts
$\mathrm{HasDerivAt},(\lambda t.,\cos\mathrm{Dihedral}(\mathrm{farCoordPath},5,t)),((4)/(8\sqrt{2})),2$.
That derivative is the slot-5 entry of the full-star deficit class kernel on the type-$(1,2)$ orbit (values $\pm\sqrt{2}/2$ on the 15 stencil classes).
In the QG campaign this is a kernel-checked increment after the type-$(1,1)$ seed orbit: star enumeration, flat cosine multiset, flatness gate $4\cdot\arccos 0=2\pi$, and the nonvacuity / swap / decoy / homothety gates all sit downstream of these path polynomials. It does not yet assemble the flat Hessian over all hinge orbits, nor close $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or gap_action_recovery. The complement type-$(2,1)$ orbit remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.