path2_polys
plain-language theorem explainer
Along the one-parameter path that varies squared-edge slot 2 about the flat Freudenthal seed, the four cleared-denominator Gram quantities (apex inner product numerator, two apex-norm numerators, and hinge Gram determinant) collapse to explicit quadratic polynomials in the path parameter. Anyone differentiating the seed-hinge dihedral cosine in slot 2 cites this identity. The proof is pure simplification and ring arithmetic on the polynomial definitions.
Claim. For every real $t$, if the ten local squared edge lengths equal the flat seed values except that slot $2$ is set to $t$, then the apex-dot numerator equals $8$, the first apex-norm-squared numerator equals $-t^2+6t-5$, the second apex-norm-squared numerator equals $8$, and the hinge Gram determinant equals $4$.
background
The module develops the dihedral-cosine kernel of the seed triangle hinge ${0,e_0,e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices, as the next kernel-checked increment after the flat Regge hinge kernel. Cosine of the dihedral angle is written in cleared-denominator Gram form: inner product and norms of the two apex vectors projected orthogonal to the hinge plane.
Four polynomial numerators appear. 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}$ respectively. The path coordPath k t freezes every local squared edge at its flat seed value except slot $k$, which is set to the real parameter $t$.
Slot 2 is one of the ten coordinate directions along which the master derivative theorem later evaluates $\partial(\cos\theta)/\partial\ell^2$ at the flat point.
proof idea
Term-mode proof. Introduce the path parameter $t$, then discharge the four conjuncts in parallel: unfold the four numerator definitions together with coordPath, simplify the resulting coordinate-wise conditionals (only slot 2 carries $t$), and finish each identity by ring. No external lemmas are required beyond the definitional equalities of the Gram numerators and the path.
why it matters
Feeds directly into hasDerivAt_cosDihedral_slot2, which asserts that the slot-2 restriction of the seed-hinge dihedral cosine has derivative $0$ at the flat point $t=3$. That theorem instantiates the generic slot derivative machine with the four coefficient triples supplied here (constant $8$ for the dot numerator, quadratic $-t^2+6t-5$ for the first apex norm, constant $8$ for the second, constant $4$ for the Gram determinant) and the positivity side-conditions checked by norm_num.
In the module deliverable list this is one of the ten coordinate-path polynomial lemmas that underwrite the full kernel cosDihedralKernel and the master statement hasDerivAt_cosDihedral_coord. Those kernels assemble, via the arccos chain factor $-\sqrt{2}$ at flat, into the two-simplex partial deficit gradient supported on edge classes $(3,7,11)$. The campaign remains strictly local: full lattice orbit sum, flat Hessian of the 4D Regge action, and $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ stay open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.