far_path2_polys
plain-language theorem explainer
Along the far-orbit edge path that varies squared-length slot 2, the four cleared-denominator Gram numerators (apex dot product, two apex norms, hinge Gram determinant) are explicit quadratic polynomials in the path parameter t. Anyone differentiating the dihedral cosine on this path cites these identities. The proof is a direct simp-and-ring expansion of the four numerator definitions on the path.
Claim. For every real $t$, if one deforms the far flat squared-edge vector by setting coordinate $2$ equal to $t$, then the apex-dot numerator equals $0$, the third-apex norm-squared numerator equals $-2t^2+12t-2$, the fourth-apex norm-squared numerator equals $4$, and the hinge Gram determinant equals $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 integer lattice. It sits in the QG campaign after the type-(1,1) seed orbit and reuses the committed Gram-projection / cleared-denominator cosine calculus.
The four quantities are the numerators that feed the dihedral cosine. hingeGramDet is $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^2$ for the hinge edge-vectors from vertex 0. apexDotNum, apex3NormSqNum, and apex4NormSqNum are the numerators of $\langle c',d'\rangle\cdot\mathrm{hingeGramDet}$, $|c'|^2\cdot\mathrm{hingeGramDet}$, and $|d'|^2\cdot\mathrm{hingeGramDet}$ for the apex projections orthogonal to the hinge plane.
farFlatSqEdges is the fixed far-orbit flat squared-length vector; farCoordPath k t replaces slot $k$ by the real parameter $t$. Here $k=2$.
proof idea
Introduce $t$, then split into the four conjuncts with refine. On each goal, unfold the four numerator definitions together with farCoordPath and farFlatSqEdges, simplify the resulting arithmetic expression, and finish by ring. No external lemmas beyond definitional expansion are required; the identities are pure polynomial equalities on the path.
why it matters
The lemma supplies the exact quadratic coefficients that hasDerivAt_far_slot2 feeds into the generic far-slot derivative theorem. That parent result shows
$\mathrm{HasDerivAt},(\lambda t.,\mathrm{cosDihedral}(\mathrm{farCoordPath},2,t)),0,1$,
i.e. the dihedral cosine is stationary at the flat point along this edge deformation.
Stationarity of the cosine on each stencil slot is part of the full-star deficit class kernel for the type-(1,2) hinge (deliverable A of the module): flat cosine multiset all zero, star angle sum exactly $2\pi$, and the $\pm\sqrt{2}/2$ kernel values on the 15 stencil classes. The module explicitly does not yet assemble the flat Hessian over all hinges, prove $S_{RS}$ converges to Einstein–Hilbert in 4D, or close gap_action_recovery; the complement orbit (2,1) remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.