path0_polys
plain-language theorem explainer
Along the one-parameter path that varies only local squared-edge slot 0 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 quadratics in the path parameter. Anyone computing the slot-0 derivative of the seed-hinge dihedral cosine cites this identity. The proof is pure definitional simplification plus ring arithmetic.
Claim. For every real $t$, if the ten local squared edge lengths equal the flat Freudenthal seed except that slot $0$ is set to $t$, then the apex-dot numerator equals $-2t^2+12t-2$, the first apex-norm numerator equals $-t^2+6t-1$, the second apex-norm numerator equals $-2t^2+12t-2$, and the hinge Gram determinant equals $-t^2+6t-1$.
background
The module treats the seed-triangle hinge inside its two Freudenthal 4-simplices as a function of the ten local squared edge lengths SqEdges4. The dihedral cosine is written in cleared-denominator Gram form: numerators for the projected apex inner product and the two projected apex norms, together with the hinge Gram determinant $4\langle a,a\rangle\langle b,b\rangle-(2\langle a,b\rangle)^2$.
The path coordPath 0 t freezes nine slots at the flat seed values and lets slot 0 equal the free parameter $t$. Section 5 of the module records that every slot restriction of the cosine is of the shape $N(t)/(2\sqrt{P(t)Q(t)})$ for quadratics $N,P,Q$ with flat values $(8,4,8)$. Establishing those quadratics for slot 0 is exactly what this lemma supplies.
Upstream definitions apexDotNum, apex3NormSqNum, apex4NormSqNum, and hingeGramDet are the explicit polynomial expressions in the ten edge slots; the lemma simply evaluates them on the path.
proof idea
Term-mode proof. Introduce the path parameter $t$, split the four conjuncts with refine, then for each conjunct unfold the four numerator/determinant definitions together with coordPath via simp and finish by ring. No external lemmas are required beyond definitional reduction and polynomial identity.
why it matters
Feeds directly into hasDerivAt_cosDihedral_slot0, which asserts that the derivative of the seed-hinge dihedral cosine along slot 0 vanishes at the flat point. That slot-0 vanishing is one of the ten coordinate derivatives packaged by the master theorem hasDerivAt_cosDihedral_coord (deliverable A of the module): slots 0–7 give derivative 0, slot 8 gives $\sqrt{2}/8$, slot 9 gives $-\sqrt{2}/4$.
Those kernels assemble, via the arccos chain rule, into the two-simplex partial deficit gradient supported on edge classes $(3,7,11)$. The module is an incremental QG kernel check after ReggeHinge4DFlatKernel; it does not yet close the full lattice orbit sum, the flat Hessian of the 4D Regge action, or S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.