t13_path7_polys
plain-language theorem explainer
Along the path that varies only squared-edge slot 7 of the type-(1,3) flat star, the four cleared-denominator Gram quantities (apex inner-product numerator, two apex-norm numerators, hinge Gram determinant) equal explicit quadratics in the path parameter. Cited by anyone assembling dihedral cosines or their derivatives for the (1,3) deficit kernel. Proof is unfold-and-ring after substituting the path into the four numerator definitions.
Claim. For every real $t$, replace squared-edge slot $7$ of the type-$(1,3)$ flat local edge tuple by $t$. Then the numerator of the projected apex inner product equals $8t-8$, the first apex-norm numerator equals $-t^{2}+8t-4$, the second apex-norm numerator equals the constant $8$, and the hinge Gram determinant equals the constant $12$.
background
The module builds the Regge 4D type-(1,3) periodic-lattice star deficit kernel: the triangle hinge with absolute masks ${0,1,15}$ (local flat squared lengths $(1,3,4)$) and its full Freudenthal star inside the origin unit cube. After vertex reordering so the hinge occupies slots $(0,1,2)$, the flat squared-edge 10-tuple is fixed; a coordinate path then replaces a single slot by a real parameter $t$ while holding the rest at those flat values.
The four quantities are the cleared-denominator numerators from the dihedral Gram-projection calculus: hinge Gram determinant $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^{2}$, and the numerators of $\langle c',d'\rangle$, $|c'|^{2}$, $|d'|^{2}$ after projecting the two apexes orthogonal to the hinge plane. At the flat point these evaluate to $(N,P,Q)=(8,8,8)$ with hinge Gram determinant $12$, the master values used for all ten slot derivatives.
proof idea
Introduce the real parameter $t$. Split the four conjuncts and, on each goal, unfold the four numerator definitions together with the coordinate path and the flat edge tuple. The resulting multivariate polynomials in $t$ are then normalized by ring, which matches the stated monic quadratics (several of which are in fact linear or constant).
why it matters
Supplies the exact polynomial coefficients that the master derivative lemma needs for slot 7. Downstream, hasDerivAt_t13_slot7 feeds those coefficients (together with the flat evaluation point $t=2$) into the cleared-denominator cosine derivative and obtains $\mathrm{HasDerivAt},(\cos\theta\circ\gamma_{7}),(3/8),2$. That derivative is one of the ten coordinate derivatives required for deliverable A of the type-(1,3) star kernel: the full-star deficit class values on classes $(1,3,5,7,9,11,13)$. The module still leaves open transport to the complementary type $(3,1)$, flat Hessian assembly over all hinges, and the global claims $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ and gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.