path4_polys
plain-language theorem explainer
Along the one-parameter path that varies squared-edge slot 4 about the flat Freudenthal seed, the four Gram numerators (apex inner product, two apex norms, hinge Gram determinant) collapse to explicit quadratics in the path parameter. Anyone computing the slot-4 derivative of the seed-hinge dihedral cosine cites this. The proof is pure simplification plus ring arithmetic after unfolding the numerator definitions.
Claim. For every real $t$, if the ten local squared edge lengths equal the flat seed values except that slot $4$ is set to $t$, then the cleared-denominator apex inner-product numerator equals $-6t^2+20t-6$, the first apex-norm numerator equals $-3t^2+10t-3$, the second apex-norm numerator equals $-4t^2+16t-4$, and the hinge Gram determinant equals $-t^2+6t-1$.
background
The module builds the Regge 4D seed-hinge dihedral cosine kernel at the flat Freudenthal point. Scope is the seed triangle hinge inside its two seed-cell 4-simplices only; the full lattice orbit sum remains open. Cosine of the dihedral angle is written via Gram projection: inner product and norms of the two apex vectors orthogonal to the hinge plane, in cleared-denominator form.
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. The three numerators apexDotNum, apex3NormSqNum, apex4NormSqNum are the corresponding cleared forms for $\langle c',d'\rangle$, $|c'|^2$, and $|d'|^2$ times that determinant. coordPath k t freezes all ten local squared edges at the flat seed except slot $k$, which is set to the real parameter $t$.
Every slot restriction of the dihedral cosine is then a rational function $N(t)/(2\sqrt{P(t)Q(t)})$ built from these four polynomials. Slot 4 is one of the ten coordinate directions whose flat derivative must be checked.
proof idea
Introduce the real parameter $t$. Split the four conjuncts with refine, then on each goal unfold apexDotNum, apex3NormSqNum, apex4NormSqNum, hingeGramDet, and coordPath. After substitution of the path (only slot 4 equals $t$; the rest are the fixed flat seed values), ring reduces each identity to a polynomial equality. No external lemmas beyond definitional unfolding.
why it matters
Feeds hasDerivAt_cosDihedral_slot4, which asserts that the derivative of the seed-hinge dihedral cosine along the slot-4 path vanishes at the flat point $t=1$. That theorem packages the four quadratic coefficients from this lemma into the generic slot derivative machine hasDerivAt_slot and converts the result to a HasDerivAt statement with value $0$.
Deliverable A of the module requires all ten coordinate derivatives of cosDihedral at flat (slots 0–7 map to $0$, slot 8 to $\sqrt{2}/8$, slot 9 to $-\sqrt{2}/4$). This lemma is the algebraic fuel for the slot-4 zero. It does not touch the Einstein–Hilbert recovery gap, the full Hessian, or the lattice orbit sum; those remain open per the module tier tags. Within the QG campaign it is a kernel-checked increment after the flat kernel module, still inside the two seed simplices only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.