t22_path0_polys
plain-language theorem explainer
Along the coordinate path that varies only the first hinge-ordered squared edge length of a type-(2,2) Regge star simplex, the four Gram-projection numerators (apex dot product, two apex norm-squares, and hinge Gram determinant) are explicit quadratic polynomials in the path parameter. Anyone computing the flat-point derivative of the dihedral cosine on this orbit cites it. The proof is a direct expand-and-ring simplification of the four numerator definitions against the path.
Claim. For every real $t$, if the squared-edge 10-tuple equals the flat type-$(2,2)$ lengths except that the $0$-th entry is set to $t$, then the apex-dot numerator equals $-2t^2+4t$, the third-apex norm-square numerator equals $-3t^2+12t-4$, the fourth-apex norm-square numerator equals $-t^2+8t-4$, and the hinge Gram determinant equals $-t^2+12t-4$.
background
This module is the type-(2,2) full-star deficit kernel for 4D Regge calculus on the periodic Freudenthal lattice. The hinge is the triangle with masks ${0,3,15}$ (difference masks $(3,12)$). Each incident simplex is encoded by a hinge-ordered 10-tuple of squared edge lengths SqEdges4.
The flat reference lengths are $(2,4,1,3,2,1,1,3,1,2)$. The coordinate path replaces a single slot $k$ by a real parameter $t$ and leaves the other nine entries at those flat values. The four scalar functions are the cleared-denominator Gram data used to build the cosine of the dihedral angle at the hinge: 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 orthogonal to the hinge plane.
These identities feed the analytic derivative of the dihedral cosine along each edge-length slot, which is the local input to the star deficit Hessian.
proof idea
Introduce the path parameter $t$. Split the four conjuncts and, on each goal, unfold the four numerator definitions together with the coordinate-path and flat-edge tables. After substitution the expressions are ordinary polynomials in $t$; ring closes each identity. No external lemmas beyond definitional unfolding are required.
why it matters
The lemma supplies the exact quadratic coefficients that hasDerivAt_t22_slot0 feeds into the generic slot-derivative theorem, yielding
$\frac{d}{dt}\cos\theta\big|_{t=2}=-1/4$
when only the $0$-th squared length is varied. That derivative is one of the fifteen stencil-class ingredients of the full-star deficit class kernel for the type-(2,2) orbit.
In the QG campaign this is the next kernel-checked increment after the type-(1,1) seed orbit. It does not yet assemble the flat Hessian over all hinges, nor does it prove continuum recovery of Einstein–Hilbert or close the gap-action flag; it only certifies the polynomial data needed for one slot of one orbit. Within Recognition Science gravity analysis it is pure discrete-geometry scaffolding toward the eight-tick / $D=3$ continuum limit, not a direct citation of the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.