t13_path2_polys
plain-language theorem explainer
Along the type-(1,3) flat edge path that varies only squared-length slot 2, the four cleared-denominator Gram numerators are explicit quadratics in the path parameter t. Anyone assembling coordinate derivatives of the dihedral cosine at the flat point cites this identity. The proof is a direct simp-and-ring expansion of the four polynomial definitions on the path.
Claim. For every real $t$, if the squared-edge 10-tuple is the type-$(1,3)$ flat configuration with only slot $2$ replaced by $t$, then the apex-dot numerator equals $8$, the first apex-norm-squared numerator equals $-3t^2+12t-4$, the second apex-norm-squared numerator equals $8$, and the hinge Gram determinant equals $12$ (each written as a quadratic in $t$).
background
This module is the QG kernel for the Regge 4D type-(1,3) periodic-lattice star: the triangle hinge with absolute masks ${0,1,15}$ and local flat squared lengths $(1,3,4)$, together with its full Freudenthal star. It sits after the type-(1,1) seed orbit and the orbit classification; it does not yet assemble the full flat Hessian or prove continuum EH recovery.
The dihedral cosine is controlled by four cleared-denominator polynomials on a squared-edge 10-tuple $a$: the hinge Gram determinant $4a_0 a_1-(a_0+a_1-a_4)^2$ (four times the squared hinge-area factor), and the three numerators of $\langle c',d'\rangle$, $|c'|^2$, and $|d'|^2$ after projecting the two apexes orthogonal to the hinge plane.
The flat reference configuration t13FlatSqEdges has those ten local squared lengths fixed after reordering so the hinge occupies slots $(0,1,2)$. The coordinate path t13CoordPath 2 t freezes every slot except slot 2, which is set to the free real parameter $t$. At the flat value one has $t=2$.
proof idea
Introduce the path parameter $t$. Split the four conjuncts with refine, then on each goal unfold the four Gram-numerator definitions together with the path and the flat edge table, and finish by ring. No external lemmas beyond those definitional expansions are required; the identities are pure polynomial arithmetic on the substituted 10-tuple.
why it matters
This identity is the polynomial fuel for hasDerivAt_t13_slot2, which feeds the cleared-denominator master derivative lemma at flat values $(N,P,Q)=(8,8,8)$ and concludes that the dihedral cosine has vanishing $t$-derivative at the flat point along slot 2. That derivative is one of the ten coordinate derivatives required for deliverable A of the type-(1,3) star kernel (flat cosine multiset, $2\pi$ angle sum, and the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$).
In the broader Recognition gravity campaign this is a kernel-checked increment toward the Regge action matching Einstein–Hilbert in 4D. It does not close gap-action recovery or $S_{\mathrm{RS}}\to\mathrm{EH}$, and transport of the kernel to the complementary type $(3,1)$ remains open. The calculation is local discrete geometry; it does not invoke the forcing chain (T5–T8), RCL, or the $\varphi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.